| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (194 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (122 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (60 entries) |
Global Index
A
and [definition, in IZF.IZF_logic]and_snd [lemma, in IZF.IZF_logic]
and_fst [lemma, in IZF.IZF_logic]
and_intro [lemma, in IZF.IZF_logic]
B
bot [definition, in IZF.IZF_logic]C
choice [axiom, in IZF.IZF_coll]Code [axiom, in IZF.IZF_coll]
COLL [definition, in IZF.IZF_coll]
coll [definition, in IZF.IZF_coll]
collection [lemma, in IZF.IZF_coll]
collection2 [lemma, in IZF.IZF_coll]
coll_rt [definition, in IZF.IZF_coll]
coll_fam [definition, in IZF.IZF_coll]
Compat [definition, in IZF.IZF_select]
D
deloc [definition, in IZF.IZF_base]E
ELT [definition, in IZF.IZF_base]ELT_compat_r [lemma, in IZF.IZF_base]
ELT_compat_l [lemma, in IZF.IZF_base]
ELT_direct [lemma, in IZF.IZF_base]
ELT_intro [lemma, in IZF.IZF_base]
eps [axiom, in IZF.IZF_coll]
eq [definition, in IZF.IZF_logic]
EQV [definition, in IZF.IZF_base]
EQV_deloc [lemma, in IZF.IZF_base]
EQV_shift [lemma, in IZF.IZF_base]
EQV_trans [lemma, in IZF.IZF_base]
EQV_sym [lemma, in IZF.IZF_base]
EQV_refl [lemma, in IZF.IZF_base]
EQV_intro [lemma, in IZF.IZF_base]
eq_out_inr [lemma, in IZF.IZF_logic]
eq_inr_out [lemma, in IZF.IZF_logic]
eq_out_inl [lemma, in IZF.IZF_logic]
eq_inl_out [lemma, in IZF.IZF_logic]
eq_inr_inl [lemma, in IZF.IZF_logic]
eq_inl_inr [lemma, in IZF.IZF_logic]
eq_inr_inr [lemma, in IZF.IZF_logic]
eq_inl_inl [lemma, in IZF.IZF_logic]
eq_none_some [lemma, in IZF.IZF_logic]
eq_some_none [lemma, in IZF.IZF_logic]
eq_some_some [lemma, in IZF.IZF_logic]
eq_trans [lemma, in IZF.IZF_logic]
eq_sym [lemma, in IZF.IZF_logic]
eq_refl [lemma, in IZF.IZF_logic]
eq_foo_in_in [lemma, in IZF.IZF_coll]
eq_foo_rt_in [lemma, in IZF.IZF_coll]
eq_foo_in_rt [lemma, in IZF.IZF_coll]
eq_S_S [lemma, in IZF.IZF_nat]
eq_O_S [lemma, in IZF.IZF_nat]
eq_S_O [lemma, in IZF.IZF_nat]
ex [definition, in IZF.IZF_logic]
exG [definition, in IZF.IZF_logic]
exG_intro [lemma, in IZF.IZF_logic]
exG_rel_intro [lemma, in IZF.IZF_coll]
exG_rel [definition, in IZF.IZF_coll]
exT [definition, in IZF.IZF_logic]
extensionality [lemma, in IZF.IZF_base]
exT_intro [lemma, in IZF.IZF_logic]
ex_intro [lemma, in IZF.IZF_logic]
ex2 [definition, in IZF.IZF_logic]
ex2_intro [lemma, in IZF.IZF_logic]
F
FOO [definition, in IZF.IZF_coll]foo [definition, in IZF.IZF_coll]
FOO_elt [lemma, in IZF.IZF_coll]
FOO_eqv [lemma, in IZF.IZF_coll]
FOO_deloc [lemma, in IZF.IZF_coll]
FOO_rt [lemma, in IZF.IZF_coll]
FOO_in [lemma, in IZF.IZF_coll]
foo_rt [definition, in IZF.IZF_coll]
foo_in [definition, in IZF.IZF_coll]
fst [definition, in IZF.IZF_nat]
I
id [definition, in IZF.IZF_omega]iff [definition, in IZF.IZF_logic]
inl [definition, in IZF.IZF_logic]
inr [definition, in IZF.IZF_logic]
IZF_select [library]
IZF_base [library]
IZF_union [library]
IZF_logic [library]
IZF_power [library]
IZF_nat [library]
IZF_pair [library]
IZF_coll [library]
IZF_omega [library]
L
LCOMPAT [definition, in IZF.IZF_coll]le [definition, in IZF.IZF_nat]
le_n_Sm [lemma, in IZF.IZF_nat]
le_inv [lemma, in IZF.IZF_nat]
le_Sn_O [lemma, in IZF.IZF_nat]
le_S [lemma, in IZF.IZF_nat]
le_trans [lemma, in IZF.IZF_nat]
le_refl [lemma, in IZF.IZF_nat]
lt [definition, in IZF.IZF_nat]
lt_n_Sm [lemma, in IZF.IZF_nat]
lt_n_O [lemma, in IZF.IZF_nat]
lt_S [lemma, in IZF.IZF_nat]
lt_n_Sn [lemma, in IZF.IZF_nat]
N
nat [definition, in IZF.IZF_nat]nat_ind' [lemma, in IZF.IZF_nat]
nat_ind [lemma, in IZF.IZF_nat]
none [definition, in IZF.IZF_logic]
O
O [definition, in IZF.IZF_nat]OMEGA [definition, in IZF.IZF_omega]
omega_ind [lemma, in IZF.IZF_omega]
omega_succ [lemma, in IZF.IZF_omega]
omega_zero [lemma, in IZF.IZF_omega]
OMEGA_SUCC [lemma, in IZF.IZF_omega]
OMEGA_ZERO [lemma, in IZF.IZF_omega]
OMEGA_rt [lemma, in IZF.IZF_omega]
OMEGA_in [lemma, in IZF.IZF_omega]
opt [definition, in IZF.IZF_logic]
or [definition, in IZF.IZF_logic]
or_inr [lemma, in IZF.IZF_logic]
or_inl [lemma, in IZF.IZF_logic]
out [definition, in IZF.IZF_logic]
P
PAIR [definition, in IZF.IZF_pair]pair [definition, in IZF.IZF_nat]
pairing [lemma, in IZF.IZF_pair]
pairing_elim [lemma, in IZF.IZF_pair]
pairing_intro2 [lemma, in IZF.IZF_pair]
pairing_intro1 [lemma, in IZF.IZF_pair]
PAIR_eqv2 [lemma, in IZF.IZF_pair]
PAIR_deloc2 [lemma, in IZF.IZF_pair]
PAIR_eqv1 [lemma, in IZF.IZF_pair]
PAIR_deloc1 [lemma, in IZF.IZF_pair]
PAIR_rt2 [lemma, in IZF.IZF_pair]
PAIR_rt1 [lemma, in IZF.IZF_pair]
PAIR_in2 [lemma, in IZF.IZF_pair]
PAIR_in1 [lemma, in IZF.IZF_pair]
POWER [definition, in IZF.IZF_power]
powerset [lemma, in IZF.IZF_power]
powerset_elim [lemma, in IZF.IZF_power]
powerset_intro [lemma, in IZF.IZF_power]
POWER_subset_eqv [lemma, in IZF.IZF_power]
POWER_eqv [lemma, in IZF.IZF_power]
POWER_deloc [lemma, in IZF.IZF_power]
POWER_rt [lemma, in IZF.IZF_power]
POWER_in2 [lemma, in IZF.IZF_power]
POWER_in1 [lemma, in IZF.IZF_power]
PRED [definition, in IZF.IZF_select]
pred [definition, in IZF.IZF_nat]
pred_S [lemma, in IZF.IZF_nat]
pred_SSn [lemma, in IZF.IZF_nat]
pred_SO [lemma, in IZF.IZF_nat]
pred_O [lemma, in IZF.IZF_nat]
R
RCOMPAT [definition, in IZF.IZF_coll]Rel [definition, in IZF.IZF_logic]
REL [definition, in IZF.IZF_coll]
S
S [definition, in IZF.IZF_nat]SELECT [definition, in IZF.IZF_select]
selection [lemma, in IZF.IZF_select]
selection_elim [lemma, in IZF.IZF_select]
selection_intro [lemma, in IZF.IZF_select]
SELECT_eqv [lemma, in IZF.IZF_select]
SELECT_deloc [lemma, in IZF.IZF_select]
SELECT_rt [lemma, in IZF.IZF_select]
SELECT_in [lemma, in IZF.IZF_select]
snd [definition, in IZF.IZF_nat]
some [definition, in IZF.IZF_logic]
sqr [definition, in IZF.IZF_nat]
step [definition, in IZF.IZF_nat]
SUB [definition, in IZF.IZF_base]
SUB_trans [lemma, in IZF.IZF_base]
SUB_refl [lemma, in IZF.IZF_base]
SUCC [definition, in IZF.IZF_omega]
successor [lemma, in IZF.IZF_omega]
SUCC_compat [lemma, in IZF.IZF_omega]
SUCC_elim [lemma, in IZF.IZF_omega]
SUCC_intro2 [lemma, in IZF.IZF_omega]
SUCC_intro1 [lemma, in IZF.IZF_omega]
SUCC_eqv [lemma, in IZF.IZF_omega]
SUCC_deloc [lemma, in IZF.IZF_omega]
SUCC_rt2 [lemma, in IZF.IZF_omega]
SUCC_rt1 [lemma, in IZF.IZF_omega]
SUCC_in [lemma, in IZF.IZF_omega]
sum [definition, in IZF.IZF_logic]
T
top [definition, in IZF.IZF_logic]top_intro [lemma, in IZF.IZF_logic]
Typ0 [definition, in IZF.IZF_nat]
Typ1 [definition, in IZF.IZF_logic]
Typ2 [definition, in IZF.IZF_logic]
U
union [lemma, in IZF.IZF_union]UNION [definition, in IZF.IZF_union]
union_elim [lemma, in IZF.IZF_union]
union_intro [lemma, in IZF.IZF_union]
UNION_eqv [lemma, in IZF.IZF_union]
UNION_deloc [lemma, in IZF.IZF_union]
UNION_rt [lemma, in IZF.IZF_union]
UNION_in [lemma, in IZF.IZF_union]
unit [definition, in IZF.IZF_omega]
W
wf_nat_S [lemma, in IZF.IZF_nat]wf_nat_O [lemma, in IZF.IZF_nat]
wf_nat [definition, in IZF.IZF_nat]
Z
ZERO [definition, in IZF.IZF_omega]ZERO_elim [lemma, in IZF.IZF_omega]
Library Index
I
IZF_selectIZF_base
IZF_union
IZF_logic
IZF_power
IZF_nat
IZF_pair
IZF_coll
IZF_omega
Lemma Index
A
and_snd [in IZF.IZF_logic]and_fst [in IZF.IZF_logic]
and_intro [in IZF.IZF_logic]
C
collection [in IZF.IZF_coll]collection2 [in IZF.IZF_coll]
E
ELT_compat_r [in IZF.IZF_base]ELT_compat_l [in IZF.IZF_base]
ELT_direct [in IZF.IZF_base]
ELT_intro [in IZF.IZF_base]
EQV_deloc [in IZF.IZF_base]
EQV_shift [in IZF.IZF_base]
EQV_trans [in IZF.IZF_base]
EQV_sym [in IZF.IZF_base]
EQV_refl [in IZF.IZF_base]
EQV_intro [in IZF.IZF_base]
eq_out_inr [in IZF.IZF_logic]
eq_inr_out [in IZF.IZF_logic]
eq_out_inl [in IZF.IZF_logic]
eq_inl_out [in IZF.IZF_logic]
eq_inr_inl [in IZF.IZF_logic]
eq_inl_inr [in IZF.IZF_logic]
eq_inr_inr [in IZF.IZF_logic]
eq_inl_inl [in IZF.IZF_logic]
eq_none_some [in IZF.IZF_logic]
eq_some_none [in IZF.IZF_logic]
eq_some_some [in IZF.IZF_logic]
eq_trans [in IZF.IZF_logic]
eq_sym [in IZF.IZF_logic]
eq_refl [in IZF.IZF_logic]
eq_foo_in_in [in IZF.IZF_coll]
eq_foo_rt_in [in IZF.IZF_coll]
eq_foo_in_rt [in IZF.IZF_coll]
eq_S_S [in IZF.IZF_nat]
eq_O_S [in IZF.IZF_nat]
eq_S_O [in IZF.IZF_nat]
exG_intro [in IZF.IZF_logic]
exG_rel_intro [in IZF.IZF_coll]
extensionality [in IZF.IZF_base]
exT_intro [in IZF.IZF_logic]
ex_intro [in IZF.IZF_logic]
ex2_intro [in IZF.IZF_logic]
F
FOO_elt [in IZF.IZF_coll]FOO_eqv [in IZF.IZF_coll]
FOO_deloc [in IZF.IZF_coll]
FOO_rt [in IZF.IZF_coll]
FOO_in [in IZF.IZF_coll]
L
le_n_Sm [in IZF.IZF_nat]le_inv [in IZF.IZF_nat]
le_Sn_O [in IZF.IZF_nat]
le_S [in IZF.IZF_nat]
le_trans [in IZF.IZF_nat]
le_refl [in IZF.IZF_nat]
lt_n_Sm [in IZF.IZF_nat]
lt_n_O [in IZF.IZF_nat]
lt_S [in IZF.IZF_nat]
lt_n_Sn [in IZF.IZF_nat]
N
nat_ind' [in IZF.IZF_nat]nat_ind [in IZF.IZF_nat]
O
omega_ind [in IZF.IZF_omega]omega_succ [in IZF.IZF_omega]
omega_zero [in IZF.IZF_omega]
OMEGA_SUCC [in IZF.IZF_omega]
OMEGA_ZERO [in IZF.IZF_omega]
OMEGA_rt [in IZF.IZF_omega]
OMEGA_in [in IZF.IZF_omega]
or_inr [in IZF.IZF_logic]
or_inl [in IZF.IZF_logic]
P
pairing [in IZF.IZF_pair]pairing_elim [in IZF.IZF_pair]
pairing_intro2 [in IZF.IZF_pair]
pairing_intro1 [in IZF.IZF_pair]
PAIR_eqv2 [in IZF.IZF_pair]
PAIR_deloc2 [in IZF.IZF_pair]
PAIR_eqv1 [in IZF.IZF_pair]
PAIR_deloc1 [in IZF.IZF_pair]
PAIR_rt2 [in IZF.IZF_pair]
PAIR_rt1 [in IZF.IZF_pair]
PAIR_in2 [in IZF.IZF_pair]
PAIR_in1 [in IZF.IZF_pair]
powerset [in IZF.IZF_power]
powerset_elim [in IZF.IZF_power]
powerset_intro [in IZF.IZF_power]
POWER_subset_eqv [in IZF.IZF_power]
POWER_eqv [in IZF.IZF_power]
POWER_deloc [in IZF.IZF_power]
POWER_rt [in IZF.IZF_power]
POWER_in2 [in IZF.IZF_power]
POWER_in1 [in IZF.IZF_power]
pred_S [in IZF.IZF_nat]
pred_SSn [in IZF.IZF_nat]
pred_SO [in IZF.IZF_nat]
pred_O [in IZF.IZF_nat]
S
selection [in IZF.IZF_select]selection_elim [in IZF.IZF_select]
selection_intro [in IZF.IZF_select]
SELECT_eqv [in IZF.IZF_select]
SELECT_deloc [in IZF.IZF_select]
SELECT_rt [in IZF.IZF_select]
SELECT_in [in IZF.IZF_select]
SUB_trans [in IZF.IZF_base]
SUB_refl [in IZF.IZF_base]
successor [in IZF.IZF_omega]
SUCC_compat [in IZF.IZF_omega]
SUCC_elim [in IZF.IZF_omega]
SUCC_intro2 [in IZF.IZF_omega]
SUCC_intro1 [in IZF.IZF_omega]
SUCC_eqv [in IZF.IZF_omega]
SUCC_deloc [in IZF.IZF_omega]
SUCC_rt2 [in IZF.IZF_omega]
SUCC_rt1 [in IZF.IZF_omega]
SUCC_in [in IZF.IZF_omega]
T
top_intro [in IZF.IZF_logic]U
union [in IZF.IZF_union]union_elim [in IZF.IZF_union]
union_intro [in IZF.IZF_union]
UNION_eqv [in IZF.IZF_union]
UNION_deloc [in IZF.IZF_union]
UNION_rt [in IZF.IZF_union]
UNION_in [in IZF.IZF_union]
W
wf_nat_S [in IZF.IZF_nat]wf_nat_O [in IZF.IZF_nat]
Z
ZERO_elim [in IZF.IZF_omega]Axiom Index
C
choice [in IZF.IZF_coll]Code [in IZF.IZF_coll]
E
eps [in IZF.IZF_coll]Definition Index
A
and [in IZF.IZF_logic]B
bot [in IZF.IZF_logic]C
COLL [in IZF.IZF_coll]coll [in IZF.IZF_coll]
coll_rt [in IZF.IZF_coll]
coll_fam [in IZF.IZF_coll]
Compat [in IZF.IZF_select]
D
deloc [in IZF.IZF_base]E
ELT [in IZF.IZF_base]eq [in IZF.IZF_logic]
EQV [in IZF.IZF_base]
ex [in IZF.IZF_logic]
exG [in IZF.IZF_logic]
exG_rel [in IZF.IZF_coll]
exT [in IZF.IZF_logic]
ex2 [in IZF.IZF_logic]
F
FOO [in IZF.IZF_coll]foo [in IZF.IZF_coll]
foo_rt [in IZF.IZF_coll]
foo_in [in IZF.IZF_coll]
fst [in IZF.IZF_nat]
I
id [in IZF.IZF_omega]iff [in IZF.IZF_logic]
inl [in IZF.IZF_logic]
inr [in IZF.IZF_logic]
L
LCOMPAT [in IZF.IZF_coll]le [in IZF.IZF_nat]
lt [in IZF.IZF_nat]
N
nat [in IZF.IZF_nat]none [in IZF.IZF_logic]
O
O [in IZF.IZF_nat]OMEGA [in IZF.IZF_omega]
opt [in IZF.IZF_logic]
or [in IZF.IZF_logic]
out [in IZF.IZF_logic]
P
PAIR [in IZF.IZF_pair]pair [in IZF.IZF_nat]
POWER [in IZF.IZF_power]
PRED [in IZF.IZF_select]
pred [in IZF.IZF_nat]
R
RCOMPAT [in IZF.IZF_coll]Rel [in IZF.IZF_logic]
REL [in IZF.IZF_coll]
S
S [in IZF.IZF_nat]SELECT [in IZF.IZF_select]
snd [in IZF.IZF_nat]
some [in IZF.IZF_logic]
sqr [in IZF.IZF_nat]
step [in IZF.IZF_nat]
SUB [in IZF.IZF_base]
SUCC [in IZF.IZF_omega]
sum [in IZF.IZF_logic]
T
top [in IZF.IZF_logic]Typ0 [in IZF.IZF_nat]
Typ1 [in IZF.IZF_logic]
Typ2 [in IZF.IZF_logic]
U
UNION [in IZF.IZF_union]unit [in IZF.IZF_omega]
W
wf_nat [in IZF.IZF_nat]Z
ZERO [in IZF.IZF_omega]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (194 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (122 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (60 entries) |