Search for blocks/addresses/...
Proofgold Asset
asset id
d772978455417a3c618207da67a31d5f44d5a83965e32287f0ee6d0402c68958
asset hash
fb35077cdbe4f1bb2aa74a5625c2eb92bba0bb4f1d65110335741700f553eb2d
bday / block
4945
tx
ed591..
preasset
doc published by
Pr6Pc..
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Definition
bij
bij
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
)
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Theorem
bijI
bijI
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
⟶
bij
x0
x1
x2
(proof)
Theorem
bijE
bijE
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
∀ x3 : ο .
(
(
∀ x4 .
x4
∈
x0
⟶
x2
x4
∈
x1
)
⟶
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x0
⟶
x2
x4
=
x2
x5
⟶
x4
=
x5
)
⟶
(
∀ x4 .
x4
∈
x1
⟶
∀ x5 : ο .
(
∀ x6 .
and
(
x6
∈
x0
)
(
x2
x6
=
x4
)
⟶
x5
)
⟶
x5
)
⟶
x3
)
⟶
x3
(proof)
Definition
equip
equip
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Known
bij_id
bij_id
:
∀ x0 .
bij
x0
x0
(
λ x1 .
x1
)
Theorem
equip_ref
equip_ref
:
∀ x0 .
equip
x0
x0
(proof)
Param
inv
inv
:
ι
→
(
ι
→
ι
) →
ι
→
ι
Known
bij_inv
bij_inv
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
bij
x1
x0
(
inv
x0
x2
)
Theorem
equip_sym
equip_sym
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
x1
x0
(proof)
Known
bij_comp
bij_comp
:
∀ x0 x1 x2 .
∀ x3 x4 :
ι → ι
.
bij
x0
x1
x3
⟶
bij
x1
x2
x4
⟶
bij
x0
x2
(
λ x5 .
x4
(
x3
x5
)
)
Theorem
equip_tra
equip_tra
:
∀ x0 x1 x2 .
equip
x0
x1
⟶
equip
x1
x2
⟶
equip
x0
x2
(proof)