| 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 | (832 entries) |
| Notation 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 | (123 entries) |
| Module 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) |
| Variable 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) |
| 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 | (3 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 | (498 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 | (93 entries) |
| Constructor 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 | (1 entry) |
| Inductive 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 | (1 entry) |
| Section 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 | (4 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 | (91 entries) |
Global Index
A
and [definition, in SetPairFunKT]and [definition, in SetPairFun]
and [definition, in SetPairFunIndPred]
andI [lemma, in SetPairFunKT]
andI [lemma, in SetPairFun]
andI [lemma, in SetPairFunIndPred]
B
binunion [definition, in SetPairFunKT]binunion [definition, in SetPairFun]
binunion [definition, in SetPairFunIndPred]
binunionE [lemma, in SetPairFunKT]
binunionE [lemma, in SetPairFun]
binunionE [lemma, in SetPairFunIndPred]
binunionEq [lemma, in SetPairFunKT]
binunionEq [lemma, in SetPairFun]
binunionEq [lemma, in SetPairFunIndPred]
binunionI1 [lemma, in SetPairFunKT]
binunionI1 [lemma, in SetPairFun]
binunionI1 [lemma, in SetPairFunIndPred]
binunionI2 [lemma, in SetPairFunKT]
binunionI2 [lemma, in SetPairFun]
binunionI2 [lemma, in SetPairFunIndPred]
C
Cond_Phi [definition, in SetPairFunKT]Cond_Phi [definition, in SetPairFun]
Cond_Phi [definition, in SetPairFunIndPred]
D
Descr [axiom, in SetPairFunKT]Descr [axiom, in SetPairFun]
Descr [axiom, in SetPairFunIndPred]
DescrR [axiom, in SetPairFunKT]
DescrR [axiom, in SetPairFun]
DescrR [axiom, in SetPairFunIndPred]
E
Empty [axiom, in SetPairFunKT]Empty [axiom, in SetPairFun]
Empty [axiom, in SetPairFunIndPred]
EmptyAx [axiom, in SetPairFunKT]
EmptyAx [axiom, in SetPairFun]
EmptyAx [axiom, in SetPairFunIndPred]
EmptyE [lemma, in SetPairFunKT]
EmptyE [lemma, in SetPairFun]
EmptyE [lemma, in SetPairFunIndPred]
Empty_Power [lemma, in SetPairFunKT]
Empty_Power [lemma, in SetPairFun]
Empty_Power [lemma, in SetPairFunIndPred]
EpsilonRec [section, in SetPairFunKT]
EpsilonRec [section, in SetPairFun]
EpsilonRec [section, in SetPairFunIndPred]
EpsilonRec.Phi [variable, in SetPairFunKT]
EpsilonRec.Phi [variable, in SetPairFun]
EpsilonRec.Phi [variable, in SetPairFunIndPred]
EpsilonRec.Phir [variable, in SetPairFunKT]
EpsilonRec.Phir [variable, in SetPairFun]
EpsilonRec.Phir [variable, in SetPairFunIndPred]
EpsilonRec.Psi [variable, in SetPairFunKT]
eq [definition, in SetPairFunKT]
eq [definition, in SetPairFun]
eq [definition, in SetPairFunIndPred]
eqI [lemma, in SetPairFunKT]
eqI [lemma, in SetPairFun]
eqI [lemma, in SetPairFunIndPred]
eq_2_Sing0 [lemma, in SetPairFunKT]
eq_1_Sing0 [lemma, in SetPairFunKT]
eq_sym [lemma, in SetPairFunKT]
eq_2_Sing0 [lemma, in SetPairFun]
eq_1_Sing0 [lemma, in SetPairFun]
eq_sym [lemma, in SetPairFun]
eq_2_Sing0 [lemma, in SetPairFunIndPred]
eq_1_Sing0 [lemma, in SetPairFunIndPred]
eq_sym [lemma, in SetPairFunIndPred]
ex [definition, in SetPairFunKT]
ex [definition, in SetPairFun]
ex [definition, in SetPairFunIndPred]
exI [lemma, in SetPairFunKT]
exI [lemma, in SetPairFun]
exI [lemma, in SetPairFunIndPred]
exI_f [lemma, in SetPairFunKT]
exI_f [lemma, in SetPairFun]
exI_f [lemma, in SetPairFunIndPred]
exu [definition, in SetPairFunKT]
exu [definition, in SetPairFun]
exu [definition, in SetPairFunIndPred]
exuI [lemma, in SetPairFunKT]
exuI [lemma, in SetPairFun]
exuI [lemma, in SetPairFunIndPred]
ex_f [definition, in SetPairFunKT]
ex_f [definition, in SetPairFun]
ex_f [definition, in SetPairFunIndPred]
F
False [definition, in SetPairFunKT]False [definition, in SetPairFun]
False [definition, in SetPairFunIndPred]
famunion [definition, in SetPairFunKT]
famunion [definition, in SetPairFun]
famunion [definition, in SetPairFunIndPred]
famunionE [lemma, in SetPairFunKT]
famunionE [lemma, in SetPairFun]
famunionE [lemma, in SetPairFunIndPred]
famunionEq [lemma, in SetPairFunKT]
famunionEq [lemma, in SetPairFun]
famunionEq [lemma, in SetPairFunIndPred]
famunionI [lemma, in SetPairFunKT]
famunionI [lemma, in SetPairFun]
famunionI [lemma, in SetPairFunIndPred]
I
iff [definition, in SetPairFunKT]iff [definition, in SetPairFun]
iff [definition, in SetPairFunIndPred]
iffI [lemma, in SetPairFunKT]
iffI [lemma, in SetPairFun]
iffI [lemma, in SetPairFunIndPred]
In [axiom, in SetPairFunKT]
In [axiom, in SetPairFun]
In [axiom, in SetPairFunIndPred]
In_rec_eq [lemma, in SetPairFunKT]
In_rec_G_In_rec_d [lemma, in SetPairFunKT]
In_rec_G_In_rec [lemma, in SetPairFunKT]
In_rec_G_f [lemma, in SetPairFunKT]
In_rec_G_c [lemma, in SetPairFunKT]
In_rec [definition, in SetPairFunKT]
In_rec_G [definition, in SetPairFunKT]
in_2_Eq [lemma, in SetPairFunKT]
in_2_E [lemma, in SetPairFunKT]
in_1_Eq [lemma, in SetPairFunKT]
in_1_E [lemma, in SetPairFunKT]
in_1_2 [lemma, in SetPairFunKT]
in_0_2 [lemma, in SetPairFunKT]
in_0_1 [lemma, in SetPairFunKT]
In_Power [lemma, in SetPairFunKT]
In_ind [axiom, in SetPairFunKT]
In_rec_eq [lemma, in SetPairFun]
In_rec_G_In_rec_d [lemma, in SetPairFun]
In_rec_G_In_rec [lemma, in SetPairFun]
In_rec_G_f [lemma, in SetPairFun]
In_rec_G_inv [lemma, in SetPairFun]
In_rec_G_ind [lemma, in SetPairFun]
In_rec_G_c [lemma, in SetPairFun]
In_rec [definition, in SetPairFun]
In_rec_G [definition, in SetPairFun]
in_2_Eq [lemma, in SetPairFun]
in_2_E [lemma, in SetPairFun]
in_1_Eq [lemma, in SetPairFun]
in_1_E [lemma, in SetPairFun]
in_1_2 [lemma, in SetPairFun]
in_0_2 [lemma, in SetPairFun]
in_0_1 [lemma, in SetPairFun]
In_Power [lemma, in SetPairFun]
In_ind [axiom, in SetPairFun]
In_rec_eq [lemma, in SetPairFunIndPred]
In_rec_G_In_rec_d [lemma, in SetPairFunIndPred]
In_rec_G_In_rec [lemma, in SetPairFunIndPred]
In_rec_G_f [lemma, in SetPairFunIndPred]
In_rec_G_inv [lemma, in SetPairFunIndPred]
In_rec [definition, in SetPairFunIndPred]
In_rec_G_c [constructor, in SetPairFunIndPred]
In_rec_G [inductive, in SetPairFunIndPred]
in_2_Eq [lemma, in SetPairFunIndPred]
in_2_E [lemma, in SetPairFunIndPred]
in_1_Eq [lemma, in SetPairFunIndPred]
in_1_E [lemma, in SetPairFunIndPred]
in_1_2 [lemma, in SetPairFunIndPred]
in_0_2 [lemma, in SetPairFunIndPred]
in_0_1 [lemma, in SetPairFunIndPred]
In_Power [lemma, in SetPairFunIndPred]
In_ind [axiom, in SetPairFunIndPred]
K
KnasterTarski [section, in SetPairFunKT]KnasterTarski.Psi [variable, in SetPairFunKT]
KnasterTarski.Psim [variable, in SetPairFunKT]
L
lfp [definition, in SetPairFunKT]lfp_eq [lemma, in SetPairFunKT]
lfp_post [lemma, in SetPairFunKT]
lfp_pre [lemma, in SetPairFunKT]
N
nat_in_dec [lemma, in SetPairFunKT]nat_ordsucc_in_ordsucc [lemma, in SetPairFunKT]
nat_trans [lemma, in SetPairFunKT]
nat_in_nat [lemma, in SetPairFunKT]
nat_0_in_ordsucc [lemma, in SetPairFunKT]
nat_complete_ind [lemma, in SetPairFunKT]
nat_inv [lemma, in SetPairFunKT]
nat_ind [lemma, in SetPairFunKT]
nat_2 [lemma, in SetPairFunKT]
nat_1 [lemma, in SetPairFunKT]
nat_ordsucc [lemma, in SetPairFunKT]
nat_0 [lemma, in SetPairFunKT]
nat_p [definition, in SetPairFunKT]
nat_in_dec [lemma, in SetPairFun]
nat_ordsucc_in_ordsucc [lemma, in SetPairFun]
nat_trans [lemma, in SetPairFun]
nat_in_nat [lemma, in SetPairFun]
nat_0_in_ordsucc [lemma, in SetPairFun]
nat_complete_ind [lemma, in SetPairFun]
nat_inv [lemma, in SetPairFun]
nat_ind [lemma, in SetPairFun]
nat_2 [lemma, in SetPairFun]
nat_1 [lemma, in SetPairFun]
nat_ordsucc [lemma, in SetPairFun]
nat_0 [lemma, in SetPairFun]
nat_p [definition, in SetPairFun]
nat_in_dec [lemma, in SetPairFunIndPred]
nat_ordsucc_in_ordsucc [lemma, in SetPairFunIndPred]
nat_trans [lemma, in SetPairFunIndPred]
nat_in_nat [lemma, in SetPairFunIndPred]
nat_0_in_ordsucc [lemma, in SetPairFunIndPred]
nat_complete_ind [lemma, in SetPairFunIndPred]
nat_inv [lemma, in SetPairFunIndPred]
nat_ind [lemma, in SetPairFunIndPred]
nat_2 [lemma, in SetPairFunIndPred]
nat_1 [lemma, in SetPairFunIndPred]
nat_ordsucc [lemma, in SetPairFunIndPred]
nat_0 [lemma, in SetPairFunIndPred]
nat_p [definition, in SetPairFunIndPred]
neq_0_1 [lemma, in SetPairFunKT]
neq_0_1 [lemma, in SetPairFun]
neq_0_1 [lemma, in SetPairFunIndPred]
not [definition, in SetPairFunKT]
not [definition, in SetPairFun]
not [definition, in SetPairFunIndPred]
O
or [definition, in SetPairFunKT]or [definition, in SetPairFun]
or [definition, in SetPairFunIndPred]
ordsucc [definition, in SetPairFunKT]
ordsucc [definition, in SetPairFun]
ordsucc [definition, in SetPairFunIndPred]
ordsuccE [lemma, in SetPairFunKT]
ordsuccE [lemma, in SetPairFun]
ordsuccE [lemma, in SetPairFunIndPred]
ordsucc_in [lemma, in SetPairFunKT]
ordsucc_Subq [lemma, in SetPairFunKT]
ordsucc_in [lemma, in SetPairFun]
ordsucc_Subq [lemma, in SetPairFun]
ordsucc_in [lemma, in SetPairFunIndPred]
ordsucc_Subq [lemma, in SetPairFunIndPred]
orIL [lemma, in SetPairFunKT]
orIL [lemma, in SetPairFun]
orIL [lemma, in SetPairFunIndPred]
orIR [lemma, in SetPairFunKT]
orIR [lemma, in SetPairFun]
orIR [lemma, in SetPairFunIndPred]
P
PairFun [module, in SetPairFunKT]PairFun [module, in SetPairFun]
PairFun [module, in SetPairFunIndPred]
PairFunConseq [module, in SetPairFunKT]
PairFunConseq [module, in SetPairFun]
PairFunConseq [module, in SetPairFunIndPred]
PairFunConseq.ap0_Sigma [lemma, in SetPairFunKT]
PairFunConseq.ap0_Sigma [lemma, in SetPairFun]
PairFunConseq.ap0_Sigma [lemma, in SetPairFunIndPred]
PairFunConseq.ap1_Sigma [lemma, in SetPairFunKT]
PairFunConseq.ap1_Sigma [lemma, in SetPairFun]
PairFunConseq.ap1_Sigma [lemma, in SetPairFunIndPred]
PairFunConseq.pair_ap_n2 [lemma, in SetPairFunKT]
PairFunConseq.pair_ap_1 [lemma, in SetPairFunKT]
PairFunConseq.pair_ap_0 [lemma, in SetPairFunKT]
PairFunConseq.pair_lam2_ex [lemma, in SetPairFunKT]
PairFunConseq.pair_ap_n2 [lemma, in SetPairFun]
PairFunConseq.pair_ap_1 [lemma, in SetPairFun]
PairFunConseq.pair_ap_0 [lemma, in SetPairFun]
PairFunConseq.pair_lam2_ex [lemma, in SetPairFun]
PairFunConseq.pair_ap_n2 [lemma, in SetPairFunIndPred]
PairFunConseq.pair_ap_1 [lemma, in SetPairFunIndPred]
PairFunConseq.pair_ap_0 [lemma, in SetPairFunIndPred]
PairFunConseq.pair_lam2_ex [lemma, in SetPairFunIndPred]
PairFunConseq.setexp_2_eq [lemma, in SetPairFunKT]
PairFunConseq.setexp_2_eq [lemma, in SetPairFun]
PairFunConseq.setexp_2_eq [lemma, in SetPairFunIndPred]
_ ^ _ [notation, in SetPairFunKT]
_ * _ [notation, in SetPairFunKT]
_ ^ _ [notation, in SetPairFun]
_ * _ [notation, in SetPairFun]
_ ^ _ [notation, in SetPairFunIndPred]
_ * _ [notation, in SetPairFunIndPred]
lambda _ : _ , _ [notation, in SetPairFunKT]
lambda _ : _ , _ [notation, in SetPairFun]
lambda _ : _ , _ [notation, in SetPairFunIndPred]
Pi _ : _ , _ [notation, in SetPairFunKT]
Pi _ : _ , _ [notation, in SetPairFun]
Pi _ : _ , _ [notation, in SetPairFunIndPred]
Sigma _ : _ , _ [notation, in SetPairFunKT]
Sigma _ : _ , _ [notation, in SetPairFun]
Sigma _ : _ , _ [notation, in SetPairFunIndPred]
( _ , _ ) [notation, in SetPairFunKT]
( _ , _ ) [notation, in SetPairFun]
( _ , _ ) [notation, in SetPairFunIndPred]
PairFunImpl [module, in SetPairFunKT]
PairFunImpl [module, in SetPairFun]
PairFunImpl [module, in SetPairFunIndPred]
PairFunImpl.ap [definition, in SetPairFunKT]
PairFunImpl.ap [definition, in SetPairFun]
PairFunImpl.ap [definition, in SetPairFunIndPred]
PairFunImpl.apE [lemma, in SetPairFunKT]
PairFunImpl.apE [lemma, in SetPairFun]
PairFunImpl.apE [lemma, in SetPairFunIndPred]
PairFunImpl.apEq [lemma, in SetPairFunKT]
PairFunImpl.apEq [lemma, in SetPairFun]
PairFunImpl.apEq [lemma, in SetPairFunIndPred]
PairFunImpl.apI [lemma, in SetPairFunKT]
PairFunImpl.apI [lemma, in SetPairFun]
PairFunImpl.apI [lemma, in SetPairFunIndPred]
PairFunImpl.ap_Pi [lemma, in SetPairFunKT]
PairFunImpl.ap_Pi [lemma, in SetPairFun]
PairFunImpl.ap_Pi [lemma, in SetPairFunIndPred]
PairFunImpl.ap0_Sigma [lemma, in SetPairFunKT]
PairFunImpl.ap0_Sigma [lemma, in SetPairFun]
PairFunImpl.ap0_Sigma [lemma, in SetPairFunIndPred]
PairFunImpl.ap1_Sigma [lemma, in SetPairFunKT]
PairFunImpl.ap1_Sigma [lemma, in SetPairFun]
PairFunImpl.ap1_Sigma [lemma, in SetPairFunIndPred]
PairFunImpl.beta [lemma, in SetPairFunKT]
PairFunImpl.beta [lemma, in SetPairFun]
PairFunImpl.beta [lemma, in SetPairFunIndPred]
PairFunImpl.beta0 [lemma, in SetPairFunKT]
PairFunImpl.beta0 [lemma, in SetPairFun]
PairFunImpl.beta0 [lemma, in SetPairFunIndPred]
PairFunImpl.Inj0 [definition, in SetPairFunKT]
PairFunImpl.Inj0 [definition, in SetPairFun]
PairFunImpl.Inj0 [definition, in SetPairFunIndPred]
PairFunImpl.Inj0E [lemma, in SetPairFunKT]
PairFunImpl.Inj0E [lemma, in SetPairFun]
PairFunImpl.Inj0E [lemma, in SetPairFunIndPred]
PairFunImpl.Inj0I [lemma, in SetPairFunKT]
PairFunImpl.Inj0I [lemma, in SetPairFun]
PairFunImpl.Inj0I [lemma, in SetPairFunIndPred]
PairFunImpl.Inj0_0 [lemma, in SetPairFunKT]
PairFunImpl.Inj0_Inj1_neq [lemma, in SetPairFunKT]
PairFunImpl.Inj0_inj [lemma, in SetPairFunKT]
PairFunImpl.Inj0_0 [lemma, in SetPairFun]
PairFunImpl.Inj0_Inj1_neq [lemma, in SetPairFun]
PairFunImpl.Inj0_inj [lemma, in SetPairFun]
PairFunImpl.Inj0_0 [lemma, in SetPairFunIndPred]
PairFunImpl.Inj0_Inj1_neq [lemma, in SetPairFunIndPred]
PairFunImpl.Inj0_inj [lemma, in SetPairFunIndPred]
PairFunImpl.Inj1 [definition, in SetPairFunKT]
PairFunImpl.Inj1 [definition, in SetPairFun]
PairFunImpl.Inj1 [definition, in SetPairFunIndPred]
PairFunImpl.Inj1E [lemma, in SetPairFunKT]
PairFunImpl.Inj1E [lemma, in SetPairFun]
PairFunImpl.Inj1E [lemma, in SetPairFunIndPred]
PairFunImpl.Inj1I1 [lemma, in SetPairFunKT]
PairFunImpl.Inj1I1 [lemma, in SetPairFun]
PairFunImpl.Inj1I1 [lemma, in SetPairFunIndPred]
PairFunImpl.Inj1I2 [lemma, in SetPairFunKT]
PairFunImpl.Inj1I2 [lemma, in SetPairFun]
PairFunImpl.Inj1I2 [lemma, in SetPairFunIndPred]
PairFunImpl.Inj1_inj [lemma, in SetPairFunKT]
PairFunImpl.Inj1_eq [lemma, in SetPairFunKT]
PairFunImpl.Inj1_inj [lemma, in SetPairFun]
PairFunImpl.Inj1_eq [lemma, in SetPairFun]
PairFunImpl.Inj1_inj [lemma, in SetPairFunIndPred]
PairFunImpl.Inj1_eq [lemma, in SetPairFunIndPred]
PairFunImpl.lam [definition, in SetPairFunKT]
PairFunImpl.lam [definition, in SetPairFun]
PairFunImpl.lam [definition, in SetPairFunIndPred]
PairFunImpl.lamE [lemma, in SetPairFunKT]
PairFunImpl.lamE [lemma, in SetPairFun]
PairFunImpl.lamE [lemma, in SetPairFunIndPred]
PairFunImpl.lamEq [lemma, in SetPairFunKT]
PairFunImpl.lamEq [lemma, in SetPairFun]
PairFunImpl.lamEq [lemma, in SetPairFunIndPred]
PairFunImpl.lamI [lemma, in SetPairFunKT]
PairFunImpl.lamI [lemma, in SetPairFun]
PairFunImpl.lamI [lemma, in SetPairFunIndPred]
PairFunImpl.lamPE [lemma, in SetPairFunKT]
PairFunImpl.lamPE [lemma, in SetPairFun]
PairFunImpl.lamPE [lemma, in SetPairFunIndPred]
PairFunImpl.lamPEq [lemma, in SetPairFunKT]
PairFunImpl.lamPEq [lemma, in SetPairFun]
PairFunImpl.lamPEq [lemma, in SetPairFunIndPred]
PairFunImpl.lam_PiEq [lemma, in SetPairFunKT]
PairFunImpl.lam_PiE [lemma, in SetPairFunKT]
PairFunImpl.lam_PiI [lemma, in SetPairFunKT]
PairFunImpl.lam_spec [lemma, in SetPairFunKT]
PairFunImpl.lam_inj [lemma, in SetPairFunKT]
PairFunImpl.lam_inj_lem [lemma, in SetPairFunKT]
PairFunImpl.lam_PiEq [lemma, in SetPairFun]
PairFunImpl.lam_PiE [lemma, in SetPairFun]
PairFunImpl.lam_PiI [lemma, in SetPairFun]
PairFunImpl.lam_spec [lemma, in SetPairFun]
PairFunImpl.lam_inj [lemma, in SetPairFun]
PairFunImpl.lam_inj_lem [lemma, in SetPairFun]
PairFunImpl.lam_PiEq [lemma, in SetPairFunIndPred]
PairFunImpl.lam_PiE [lemma, in SetPairFunIndPred]
PairFunImpl.lam_PiI [lemma, in SetPairFunIndPred]
PairFunImpl.lam_spec [lemma, in SetPairFunIndPred]
PairFunImpl.lam_inj [lemma, in SetPairFunIndPred]
PairFunImpl.lam_inj_lem [lemma, in SetPairFunIndPred]
PairFunImpl.lam2_pair [lemma, in SetPairFunKT]
PairFunImpl.lam2_pair [lemma, in SetPairFun]
PairFunImpl.lam2_pair [lemma, in SetPairFunIndPred]
PairFunImpl.nat_sum1_ordsucc [lemma, in SetPairFunKT]
PairFunImpl.nat_pair1_ordsucc [lemma, in SetPairFunKT]
PairFunImpl.nat_in_setexp_mon [lemma, in SetPairFunKT]
PairFunImpl.nat_sum1_ordsucc [lemma, in SetPairFun]
PairFunImpl.nat_pair1_ordsucc [lemma, in SetPairFun]
PairFunImpl.nat_in_setexp_mon [lemma, in SetPairFun]
PairFunImpl.nat_sum1_ordsucc [lemma, in SetPairFunIndPred]
PairFunImpl.nat_pair1_ordsucc [lemma, in SetPairFunIndPred]
PairFunImpl.nat_in_setexp_mon [lemma, in SetPairFunIndPred]
PairFunImpl.pair [definition, in SetPairFunKT]
PairFunImpl.pair [definition, in SetPairFun]
PairFunImpl.pair [definition, in SetPairFunIndPred]
PairFunImpl.pairE [lemma, in SetPairFunKT]
PairFunImpl.pairE [lemma, in SetPairFun]
PairFunImpl.pairE [lemma, in SetPairFunIndPred]
PairFunImpl.pairEq [lemma, in SetPairFunKT]
PairFunImpl.pairEq [lemma, in SetPairFun]
PairFunImpl.pairEq [lemma, in SetPairFunIndPred]
PairFunImpl.pairE0 [lemma, in SetPairFunKT]
PairFunImpl.pairE0 [lemma, in SetPairFun]
PairFunImpl.pairE0 [lemma, in SetPairFunIndPred]
PairFunImpl.pairE1 [lemma, in SetPairFunKT]
PairFunImpl.pairE1 [lemma, in SetPairFun]
PairFunImpl.pairE1 [lemma, in SetPairFunIndPred]
PairFunImpl.pairI0 [lemma, in SetPairFunKT]
PairFunImpl.pairI0 [lemma, in SetPairFun]
PairFunImpl.pairI0 [lemma, in SetPairFunIndPred]
PairFunImpl.pairI1 [lemma, in SetPairFunKT]
PairFunImpl.pairI1 [lemma, in SetPairFun]
PairFunImpl.pairI1 [lemma, in SetPairFunIndPred]
PairFunImpl.pairSubq [lemma, in SetPairFunKT]
PairFunImpl.pairSubq [lemma, in SetPairFun]
PairFunImpl.pairSubq [lemma, in SetPairFunIndPred]
PairFunImpl.pair_1_1_2 [lemma, in SetPairFunKT]
PairFunImpl.pair_1_0_1 [lemma, in SetPairFunKT]
PairFunImpl.pair_SigmaEq [lemma, in SetPairFunKT]
PairFunImpl.pair_SigmaE [lemma, in SetPairFunKT]
PairFunImpl.pair_SigmaI [lemma, in SetPairFunKT]
PairFunImpl.pair_ap_n2 [lemma, in SetPairFunKT]
PairFunImpl.pair_ap_1 [lemma, in SetPairFunKT]
PairFunImpl.pair_ap_0 [lemma, in SetPairFunKT]
PairFunImpl.pair_spec [lemma, in SetPairFunKT]
PairFunImpl.pair_inj [lemma, in SetPairFunKT]
PairFunImpl.pair_inj_Subq_1 [lemma, in SetPairFunKT]
PairFunImpl.pair_inj_Subq_0 [lemma, in SetPairFunKT]
PairFunImpl.pair_0_1_neq [lemma, in SetPairFunKT]
PairFunImpl.pair_1_inj [lemma, in SetPairFunKT]
PairFunImpl.pair_0_inj [lemma, in SetPairFunKT]
PairFunImpl.pair_1_x [lemma, in SetPairFunKT]
PairFunImpl.pair_0_x [lemma, in SetPairFunKT]
PairFunImpl.pair_0_0 [lemma, in SetPairFunKT]
PairFunImpl.pair_1_1_2 [lemma, in SetPairFun]
PairFunImpl.pair_1_0_1 [lemma, in SetPairFun]
PairFunImpl.pair_SigmaEq [lemma, in SetPairFun]
PairFunImpl.pair_SigmaE [lemma, in SetPairFun]
PairFunImpl.pair_SigmaI [lemma, in SetPairFun]
PairFunImpl.pair_ap_n2 [lemma, in SetPairFun]
PairFunImpl.pair_ap_1 [lemma, in SetPairFun]
PairFunImpl.pair_ap_0 [lemma, in SetPairFun]
PairFunImpl.pair_spec [lemma, in SetPairFun]
PairFunImpl.pair_inj [lemma, in SetPairFun]
PairFunImpl.pair_inj_Subq_1 [lemma, in SetPairFun]
PairFunImpl.pair_inj_Subq_0 [lemma, in SetPairFun]
PairFunImpl.pair_0_1_neq [lemma, in SetPairFun]
PairFunImpl.pair_1_inj [lemma, in SetPairFun]
PairFunImpl.pair_0_inj [lemma, in SetPairFun]
PairFunImpl.pair_1_x [lemma, in SetPairFun]
PairFunImpl.pair_0_x [lemma, in SetPairFun]
PairFunImpl.pair_0_0 [lemma, in SetPairFun]
PairFunImpl.pair_1_1_2 [lemma, in SetPairFunIndPred]
PairFunImpl.pair_1_0_1 [lemma, in SetPairFunIndPred]
PairFunImpl.pair_SigmaEq [lemma, in SetPairFunIndPred]
PairFunImpl.pair_SigmaE [lemma, in SetPairFunIndPred]
PairFunImpl.pair_SigmaI [lemma, in SetPairFunIndPred]
PairFunImpl.pair_ap_n2 [lemma, in SetPairFunIndPred]
PairFunImpl.pair_ap_1 [lemma, in SetPairFunIndPred]
PairFunImpl.pair_ap_0 [lemma, in SetPairFunIndPred]
PairFunImpl.pair_spec [lemma, in SetPairFunIndPred]
PairFunImpl.pair_inj [lemma, in SetPairFunIndPred]
PairFunImpl.pair_inj_Subq_1 [lemma, in SetPairFunIndPred]
PairFunImpl.pair_inj_Subq_0 [lemma, in SetPairFunIndPred]
PairFunImpl.pair_0_1_neq [lemma, in SetPairFunIndPred]
PairFunImpl.pair_1_inj [lemma, in SetPairFunIndPred]
PairFunImpl.pair_0_inj [lemma, in SetPairFunIndPred]
PairFunImpl.pair_1_x [lemma, in SetPairFunIndPred]
PairFunImpl.pair_0_x [lemma, in SetPairFunIndPred]
PairFunImpl.pair_0_0 [lemma, in SetPairFunIndPred]
PairFunImpl.pair0_sum [lemma, in SetPairFunKT]
PairFunImpl.pair0_sum [lemma, in SetPairFun]
PairFunImpl.pair0_sum [lemma, in SetPairFunIndPred]
PairFunImpl.pair1_sum [lemma, in SetPairFunKT]
PairFunImpl.pair1_sum [lemma, in SetPairFun]
PairFunImpl.pair1_sum [lemma, in SetPairFunIndPred]
PairFunImpl.PI [definition, in SetPairFunKT]
PairFunImpl.PI [definition, in SetPairFun]
PairFunImpl.PI [definition, in SetPairFunIndPred]
PairFunImpl.Pi_0_mon [lemma, in SetPairFunKT]
PairFunImpl.Pi_cod_mon [lemma, in SetPairFunKT]
PairFunImpl.Pi_0_dom_mon [lemma, in SetPairFunKT]
PairFunImpl.Pi_Power_1 [lemma, in SetPairFunKT]
PairFunImpl.Pi_eta [lemma, in SetPairFunKT]
PairFunImpl.Pi_0_mon [lemma, in SetPairFun]
PairFunImpl.Pi_cod_mon [lemma, in SetPairFun]
PairFunImpl.Pi_0_dom_mon [lemma, in SetPairFun]
PairFunImpl.Pi_Power_1 [lemma, in SetPairFun]
PairFunImpl.Pi_eta [lemma, in SetPairFun]
PairFunImpl.Pi_0_mon [lemma, in SetPairFunIndPred]
PairFunImpl.Pi_cod_mon [lemma, in SetPairFunIndPred]
PairFunImpl.Pi_0_dom_mon [lemma, in SetPairFunIndPred]
PairFunImpl.Pi_Power_1 [lemma, in SetPairFunIndPred]
PairFunImpl.Pi_eta [lemma, in SetPairFunIndPred]
PairFunImpl.setexp_0_mon [lemma, in SetPairFunKT]
PairFunImpl.setexp_0_dom_mon [lemma, in SetPairFunKT]
PairFunImpl.setexp_2_eq [lemma, in SetPairFunKT]
PairFunImpl.setexp_0_mon [lemma, in SetPairFun]
PairFunImpl.setexp_0_dom_mon [lemma, in SetPairFun]
PairFunImpl.setexp_2_eq [lemma, in SetPairFun]
PairFunImpl.setexp_0_mon [lemma, in SetPairFunIndPred]
PairFunImpl.setexp_0_dom_mon [lemma, in SetPairFunIndPred]
PairFunImpl.setexp_2_eq [lemma, in SetPairFunIndPred]
PairFunImpl.SIGMA [definition, in SetPairFunKT]
PairFunImpl.SIGMA [definition, in SetPairFun]
PairFunImpl.SIGMA [definition, in SetPairFunIndPred]
PairFunImpl.Sigma_mon1 [lemma, in SetPairFunKT]
PairFunImpl.Sigma_mon0 [lemma, in SetPairFunKT]
PairFunImpl.Sigma_mon [lemma, in SetPairFunKT]
PairFunImpl.Sigma_Power_1 [lemma, in SetPairFunKT]
PairFunImpl.Sigma_eta [lemma, in SetPairFunKT]
PairFunImpl.Sigma_mon1 [lemma, in SetPairFun]
PairFunImpl.Sigma_mon0 [lemma, in SetPairFun]
PairFunImpl.Sigma_mon [lemma, in SetPairFun]
PairFunImpl.Sigma_Power_1 [lemma, in SetPairFun]
PairFunImpl.Sigma_eta [lemma, in SetPairFun]
PairFunImpl.Sigma_mon1 [lemma, in SetPairFunIndPred]
PairFunImpl.Sigma_mon0 [lemma, in SetPairFunIndPred]
PairFunImpl.Sigma_mon [lemma, in SetPairFunIndPred]
PairFunImpl.Sigma_Power_1 [lemma, in SetPairFunIndPred]
PairFunImpl.Sigma_eta [lemma, in SetPairFunIndPred]
PairFunImpl.sum [definition, in SetPairFunKT]
PairFunImpl.sum [definition, in SetPairFun]
PairFunImpl.sum [definition, in SetPairFunIndPred]
PairFunImpl.sumEq [lemma, in SetPairFunKT]
PairFunImpl.sumEq [lemma, in SetPairFun]
PairFunImpl.sumEq [lemma, in SetPairFunIndPred]
PairFunImpl.sum_mon [lemma, in SetPairFunKT]
PairFunImpl.sum_1_1_2 [lemma, in SetPairFunKT]
PairFunImpl.sum_1_0_1 [lemma, in SetPairFunKT]
PairFunImpl.sum_inv [lemma, in SetPairFunKT]
PairFunImpl.sum_mon [lemma, in SetPairFun]
PairFunImpl.sum_1_1_2 [lemma, in SetPairFun]
PairFunImpl.sum_1_0_1 [lemma, in SetPairFun]
PairFunImpl.sum_inv [lemma, in SetPairFun]
PairFunImpl.sum_mon [lemma, in SetPairFunIndPred]
PairFunImpl.sum_1_1_2 [lemma, in SetPairFunIndPred]
PairFunImpl.sum_1_0_1 [lemma, in SetPairFunIndPred]
PairFunImpl.sum_inv [lemma, in SetPairFunIndPred]
PairFunImpl.Unj [definition, in SetPairFunKT]
PairFunImpl.Unj [definition, in SetPairFun]
PairFunImpl.Unj [definition, in SetPairFunIndPred]
PairFunImpl.Unj_Inj0_eq [lemma, in SetPairFunKT]
PairFunImpl.Unj_Inj1_eq [lemma, in SetPairFunKT]
PairFunImpl.Unj_eq [lemma, in SetPairFunKT]
PairFunImpl.Unj_Inj0_eq [lemma, in SetPairFun]
PairFunImpl.Unj_Inj1_eq [lemma, in SetPairFun]
PairFunImpl.Unj_eq [lemma, in SetPairFun]
PairFunImpl.Unj_Inj0_eq [lemma, in SetPairFunIndPred]
PairFunImpl.Unj_Inj1_eq [lemma, in SetPairFunIndPred]
PairFunImpl.Unj_eq [lemma, in SetPairFunIndPred]
_ :+: _ [notation, in SetPairFunKT]
_ ^ _ [notation, in SetPairFunKT]
_ * _ [notation, in SetPairFunKT]
_ :+: _ [notation, in SetPairFun]
_ ^ _ [notation, in SetPairFun]
_ * _ [notation, in SetPairFun]
_ :+: _ [notation, in SetPairFunIndPred]
_ ^ _ [notation, in SetPairFunIndPred]
_ * _ [notation, in SetPairFunIndPred]
lambda _ : _ , _ [notation, in SetPairFunKT]
lambda _ : _ , _ [notation, in SetPairFun]
lambda _ : _ , _ [notation, in SetPairFunIndPred]
Pi _ : _ , _ [notation, in SetPairFunKT]
Pi _ : _ , _ [notation, in SetPairFun]
Pi _ : _ , _ [notation, in SetPairFunIndPred]
Sigma _ : _ , _ [notation, in SetPairFunKT]
Sigma _ : _ , _ [notation, in SetPairFun]
Sigma _ : _ , _ [notation, in SetPairFunIndPred]
( _ , _ ) [notation, in SetPairFunKT]
( _ , _ ) [notation, in SetPairFun]
( _ , _ ) [notation, in SetPairFunIndPred]
PairFun.ap [axiom, in SetPairFunKT]
PairFun.ap [axiom, in SetPairFun]
PairFun.ap [axiom, in SetPairFunIndPred]
PairFun.ap_Pi [axiom, in SetPairFunKT]
PairFun.ap_Pi [axiom, in SetPairFun]
PairFun.ap_Pi [axiom, in SetPairFunIndPred]
PairFun.beta [axiom, in SetPairFunKT]
PairFun.beta [axiom, in SetPairFun]
PairFun.beta [axiom, in SetPairFunIndPred]
PairFun.beta0 [axiom, in SetPairFunKT]
PairFun.beta0 [axiom, in SetPairFun]
PairFun.beta0 [axiom, in SetPairFunIndPred]
PairFun.lam [axiom, in SetPairFunKT]
PairFun.lam [axiom, in SetPairFun]
PairFun.lam [axiom, in SetPairFunIndPred]
PairFun.lam_PiEq [axiom, in SetPairFunKT]
PairFun.lam_spec [axiom, in SetPairFunKT]
PairFun.lam_PiEq [axiom, in SetPairFun]
PairFun.lam_spec [axiom, in SetPairFun]
PairFun.lam_PiEq [axiom, in SetPairFunIndPred]
PairFun.lam_spec [axiom, in SetPairFunIndPred]
PairFun.lam2_pair [axiom, in SetPairFunKT]
PairFun.lam2_pair [axiom, in SetPairFun]
PairFun.lam2_pair [axiom, in SetPairFunIndPred]
PairFun.pair [axiom, in SetPairFunKT]
PairFun.pair [axiom, in SetPairFun]
PairFun.pair [axiom, in SetPairFunIndPred]
PairFun.pair_SigmaEq [axiom, in SetPairFunKT]
PairFun.pair_spec [axiom, in SetPairFunKT]
PairFun.pair_SigmaEq [axiom, in SetPairFun]
PairFun.pair_spec [axiom, in SetPairFun]
PairFun.pair_SigmaEq [axiom, in SetPairFunIndPred]
PairFun.pair_spec [axiom, in SetPairFunIndPred]
PairFun.PI [axiom, in SetPairFunKT]
PairFun.PI [axiom, in SetPairFun]
PairFun.PI [axiom, in SetPairFunIndPred]
PairFun.Pi_Power_1 [axiom, in SetPairFunKT]
PairFun.Pi_Power_1 [axiom, in SetPairFun]
PairFun.Pi_Power_1 [axiom, in SetPairFunIndPred]
PairFun.SIGMA [axiom, in SetPairFunKT]
PairFun.SIGMA [axiom, in SetPairFun]
PairFun.SIGMA [axiom, in SetPairFunIndPred]
PairFun.Sigma_Power_1 [axiom, in SetPairFunKT]
PairFun.Sigma_Power_1 [axiom, in SetPairFun]
PairFun.Sigma_Power_1 [axiom, in SetPairFunIndPred]
lambda _ : _ , _ [notation, in SetPairFunKT]
lambda _ : _ , _ [notation, in SetPairFun]
lambda _ : _ , _ [notation, in SetPairFunIndPred]
Pi _ : _ , _ [notation, in SetPairFunKT]
Pi _ : _ , _ [notation, in SetPairFun]
Pi _ : _ , _ [notation, in SetPairFunIndPred]
Sigma _ : _ , _ [notation, in SetPairFunKT]
Sigma _ : _ , _ [notation, in SetPairFun]
Sigma _ : _ , _ [notation, in SetPairFunIndPred]
( _ , _ ) [notation, in SetPairFunKT]
( _ , _ ) [notation, in SetPairFun]
( _ , _ ) [notation, in SetPairFunIndPred]
PhiPsim [lemma, in SetPairFunKT]
Power [axiom, in SetPairFunKT]
Power [axiom, in SetPairFun]
Power [axiom, in SetPairFunIndPred]
PowerE [lemma, in SetPairFunKT]
PowerE [lemma, in SetPairFun]
PowerE [lemma, in SetPairFunIndPred]
PowerEq [axiom, in SetPairFunKT]
PowerEq [axiom, in SetPairFun]
PowerEq [axiom, in SetPairFunIndPred]
PowerI [lemma, in SetPairFunKT]
PowerI [lemma, in SetPairFun]
PowerI [lemma, in SetPairFunIndPred]
Psi_monotone [definition, in SetPairFunKT]
R
Repl [axiom, in SetPairFunKT]Repl [axiom, in SetPairFun]
Repl [axiom, in SetPairFunIndPred]
ReplE [lemma, in SetPairFunKT]
ReplE [lemma, in SetPairFun]
ReplE [lemma, in SetPairFunIndPred]
ReplEq [axiom, in SetPairFunKT]
ReplEq [axiom, in SetPairFun]
ReplEq [axiom, in SetPairFunIndPred]
ReplI [lemma, in SetPairFunKT]
ReplI [lemma, in SetPairFun]
ReplI [lemma, in SetPairFunIndPred]
Repl_Empty [lemma, in SetPairFunKT]
Repl_restr [lemma, in SetPairFunKT]
Repl_restr_1 [lemma, in SetPairFunKT]
Repl_Empty [lemma, in SetPairFun]
Repl_restr [lemma, in SetPairFun]
Repl_restr_1 [lemma, in SetPairFun]
Repl_Empty [lemma, in SetPairFunIndPred]
Repl_restr [lemma, in SetPairFunIndPred]
Repl_restr_1 [lemma, in SetPairFunIndPred]
S
Sep [axiom, in SetPairFunKT]Sep [axiom, in SetPairFun]
Sep [axiom, in SetPairFunIndPred]
SepE [lemma, in SetPairFunKT]
SepE [lemma, in SetPairFun]
SepE [lemma, in SetPairFunIndPred]
SepEq [axiom, in SetPairFunKT]
SepEq [axiom, in SetPairFun]
SepEq [axiom, in SetPairFunIndPred]
SepE1 [lemma, in SetPairFunKT]
SepE1 [lemma, in SetPairFun]
SepE1 [lemma, in SetPairFunIndPred]
SepE2 [lemma, in SetPairFunKT]
SepE2 [lemma, in SetPairFun]
SepE2 [lemma, in SetPairFunIndPred]
SepI [lemma, in SetPairFunKT]
SepI [lemma, in SetPairFun]
SepI [lemma, in SetPairFunIndPred]
set [axiom, in SetPairFunKT]
set [axiom, in SetPairFun]
set [axiom, in SetPairFunIndPred]
setminus [definition, in SetPairFunKT]
setminus [definition, in SetPairFun]
setminus [definition, in SetPairFunIndPred]
setminusEq [lemma, in SetPairFunKT]
setminusEq [lemma, in SetPairFun]
setminusEq [lemma, in SetPairFunIndPred]
setminusE1 [lemma, in SetPairFunKT]
setminusE1 [lemma, in SetPairFun]
setminusE1 [lemma, in SetPairFunIndPred]
setminusE2 [lemma, in SetPairFunKT]
setminusE2 [lemma, in SetPairFun]
setminusE2 [lemma, in SetPairFunIndPred]
setminusI [lemma, in SetPairFunKT]
setminusI [lemma, in SetPairFun]
setminusI [lemma, in SetPairFunIndPred]
SetPairFun [library]
SetPairFunIndPred [library]
SetPairFunKT [library]
set_ext [axiom, in SetPairFunKT]
set_ext [axiom, in SetPairFun]
set_ext [axiom, in SetPairFunIndPred]
Sing [definition, in SetPairFunKT]
Sing [definition, in SetPairFun]
Sing [definition, in SetPairFunIndPred]
SingE [lemma, in SetPairFunKT]
SingE [lemma, in SetPairFun]
SingE [lemma, in SetPairFunIndPred]
SingEq [lemma, in SetPairFunKT]
SingEq [lemma, in SetPairFun]
SingEq [lemma, in SetPairFunIndPred]
SingI [lemma, in SetPairFunKT]
SingI [lemma, in SetPairFun]
SingI [lemma, in SetPairFunIndPred]
Subq [definition, in SetPairFunKT]
Subq [definition, in SetPairFun]
Subq [definition, in SetPairFunIndPred]
Subq_Empty [lemma, in SetPairFunKT]
Subq_tra [lemma, in SetPairFunKT]
Subq_ref [lemma, in SetPairFunKT]
Subq_Empty [lemma, in SetPairFun]
Subq_tra [lemma, in SetPairFun]
Subq_ref [lemma, in SetPairFun]
Subq_Empty [lemma, in SetPairFunIndPred]
Subq_tra [lemma, in SetPairFunIndPred]
Subq_ref [lemma, in SetPairFunIndPred]
T
TSet [definition, in SetPairFunKT]TSet [definition, in SetPairFun]
TSet [definition, in SetPairFunIndPred]
U
Union [axiom, in SetPairFunKT]Union [axiom, in SetPairFun]
Union [axiom, in SetPairFunIndPred]
UnionE [lemma, in SetPairFunKT]
UnionE [lemma, in SetPairFun]
UnionE [lemma, in SetPairFunIndPred]
UnionEq [axiom, in SetPairFunKT]
UnionEq [axiom, in SetPairFun]
UnionEq [axiom, in SetPairFunIndPred]
UnionI [lemma, in SetPairFunKT]
UnionI [lemma, in SetPairFun]
UnionI [lemma, in SetPairFunIndPred]
UPair [definition, in SetPairFunKT]
UPair [definition, in SetPairFun]
UPair [definition, in SetPairFunIndPred]
UPairE [lemma, in SetPairFunKT]
UPairE [lemma, in SetPairFun]
UPairE [lemma, in SetPairFunIndPred]
UPairEq [lemma, in SetPairFunKT]
UPairEq [lemma, in SetPairFun]
UPairEq [lemma, in SetPairFunIndPred]
UPairI1 [lemma, in SetPairFunKT]
UPairI1 [lemma, in SetPairFun]
UPairI1 [lemma, in SetPairFunIndPred]
UPairI2 [lemma, in SetPairFunKT]
UPairI2 [lemma, in SetPairFun]
UPairI2 [lemma, in SetPairFunIndPred]
other
_ + [notation, in SetPairFunKT]_ \ _ [notation, in SetPairFunKT]
_ :u: _ [notation, in SetPairFunKT]
_ /c= _ [notation, in SetPairFunKT]
_ c= _ [notation, in SetPairFunKT]
_ /:e _ [notation, in SetPairFunKT]
_ :e _ [notation, in SetPairFunKT]
_ <> _ [notation, in SetPairFunKT]
_ = _ [notation, in SetPairFunKT]
_ <-> _ [notation, in SetPairFunKT]
_ \/ _ [notation, in SetPairFunKT]
_ /\ _ [notation, in SetPairFunKT]
_ + [notation, in SetPairFun]
_ \ _ [notation, in SetPairFun]
_ :u: _ [notation, in SetPairFun]
_ /c= _ [notation, in SetPairFun]
_ c= _ [notation, in SetPairFun]
_ /:e _ [notation, in SetPairFun]
_ :e _ [notation, in SetPairFun]
_ <> _ [notation, in SetPairFun]
_ = _ [notation, in SetPairFun]
_ <-> _ [notation, in SetPairFun]
_ \/ _ [notation, in SetPairFun]
_ /\ _ [notation, in SetPairFun]
_ + [notation, in SetPairFunIndPred]
_ \ _ [notation, in SetPairFunIndPred]
_ :u: _ [notation, in SetPairFunIndPred]
_ /c= _ [notation, in SetPairFunIndPred]
_ c= _ [notation, in SetPairFunIndPred]
_ /:e _ [notation, in SetPairFunIndPred]
_ :e _ [notation, in SetPairFunIndPred]
_ <> _ [notation, in SetPairFunIndPred]
_ = _ [notation, in SetPairFunIndPred]
_ <-> _ [notation, in SetPairFunIndPred]
_ \/ _ [notation, in SetPairFunIndPred]
_ /\ _ [notation, in SetPairFunIndPred]
existsf _ , _ [notation, in SetPairFunKT]
existsf _ , _ [notation, in SetPairFun]
existsf _ , _ [notation, in SetPairFunIndPred]
exists! _ , _ [notation, in SetPairFunKT]
exists! _ , _ [notation, in SetPairFun]
exists! _ , _ [notation, in SetPairFunIndPred]
exists _ , _ [notation, in SetPairFunKT]
exists _ , _ [notation, in SetPairFun]
exists _ , _ [notation, in SetPairFunIndPred]
U _ : _ , _ [notation, in SetPairFunKT]
U _ : _ , _ [notation, in SetPairFun]
U _ : _ , _ [notation, in SetPairFunIndPred]
0 [notation, in SetPairFunKT]
0 [notation, in SetPairFun]
0 [notation, in SetPairFunIndPred]
1 [notation, in SetPairFunKT]
1 [notation, in SetPairFun]
1 [notation, in SetPairFunIndPred]
2 [notation, in SetPairFunKT]
2 [notation, in SetPairFun]
2 [notation, in SetPairFunIndPred]
{ _ , _ } [notation, in SetPairFunKT]
{ _ | _ :i _ } [notation, in SetPairFunKT]
{ _ :i _ | _ } [notation, in SetPairFunKT]
{ _ , _ } [notation, in SetPairFun]
{ _ | _ :i _ } [notation, in SetPairFun]
{ _ :i _ | _ } [notation, in SetPairFun]
{ _ , _ } [notation, in SetPairFunIndPred]
{ _ | _ :i _ } [notation, in SetPairFunIndPred]
{ _ :i _ | _ } [notation, in SetPairFunIndPred]
{| _ |} [notation, in SetPairFunKT]
{| _ |} [notation, in SetPairFun]
{| _ |} [notation, in SetPairFunIndPred]
~ _ [notation, in SetPairFunKT]
~ _ [notation, in SetPairFun]
~ _ [notation, in SetPairFunIndPred]
Notation Index
P
_ ^ _ [in SetPairFunKT]_ * _ [in SetPairFunKT]
_ ^ _ [in SetPairFun]
_ * _ [in SetPairFun]
_ ^ _ [in SetPairFunIndPred]
_ * _ [in SetPairFunIndPred]
lambda _ : _ , _ [in SetPairFunKT]
lambda _ : _ , _ [in SetPairFun]
lambda _ : _ , _ [in SetPairFunIndPred]
Pi _ : _ , _ [in SetPairFunKT]
Pi _ : _ , _ [in SetPairFun]
Pi _ : _ , _ [in SetPairFunIndPred]
Sigma _ : _ , _ [in SetPairFunKT]
Sigma _ : _ , _ [in SetPairFun]
Sigma _ : _ , _ [in SetPairFunIndPred]
( _ , _ ) [in SetPairFunKT]
( _ , _ ) [in SetPairFun]
( _ , _ ) [in SetPairFunIndPred]
_ :+: _ [in SetPairFunKT]
_ ^ _ [in SetPairFunKT]
_ * _ [in SetPairFunKT]
_ :+: _ [in SetPairFun]
_ ^ _ [in SetPairFun]
_ * _ [in SetPairFun]
_ :+: _ [in SetPairFunIndPred]
_ ^ _ [in SetPairFunIndPred]
_ * _ [in SetPairFunIndPred]
lambda _ : _ , _ [in SetPairFunKT]
lambda _ : _ , _ [in SetPairFun]
lambda _ : _ , _ [in SetPairFunIndPred]
Pi _ : _ , _ [in SetPairFunKT]
Pi _ : _ , _ [in SetPairFun]
Pi _ : _ , _ [in SetPairFunIndPred]
Sigma _ : _ , _ [in SetPairFunKT]
Sigma _ : _ , _ [in SetPairFun]
Sigma _ : _ , _ [in SetPairFunIndPred]
( _ , _ ) [in SetPairFunKT]
( _ , _ ) [in SetPairFun]
( _ , _ ) [in SetPairFunIndPred]
lambda _ : _ , _ [in SetPairFunKT]
lambda _ : _ , _ [in SetPairFun]
lambda _ : _ , _ [in SetPairFunIndPred]
Pi _ : _ , _ [in SetPairFunKT]
Pi _ : _ , _ [in SetPairFun]
Pi _ : _ , _ [in SetPairFunIndPred]
Sigma _ : _ , _ [in SetPairFunKT]
Sigma _ : _ , _ [in SetPairFun]
Sigma _ : _ , _ [in SetPairFunIndPred]
( _ , _ ) [in SetPairFunKT]
( _ , _ ) [in SetPairFun]
( _ , _ ) [in SetPairFunIndPred]
other
_ + [in SetPairFunKT]_ \ _ [in SetPairFunKT]
_ :u: _ [in SetPairFunKT]
_ /c= _ [in SetPairFunKT]
_ c= _ [in SetPairFunKT]
_ /:e _ [in SetPairFunKT]
_ :e _ [in SetPairFunKT]
_ <> _ [in SetPairFunKT]
_ = _ [in SetPairFunKT]
_ <-> _ [in SetPairFunKT]
_ \/ _ [in SetPairFunKT]
_ /\ _ [in SetPairFunKT]
_ + [in SetPairFun]
_ \ _ [in SetPairFun]
_ :u: _ [in SetPairFun]
_ /c= _ [in SetPairFun]
_ c= _ [in SetPairFun]
_ /:e _ [in SetPairFun]
_ :e _ [in SetPairFun]
_ <> _ [in SetPairFun]
_ = _ [in SetPairFun]
_ <-> _ [in SetPairFun]
_ \/ _ [in SetPairFun]
_ /\ _ [in SetPairFun]
_ + [in SetPairFunIndPred]
_ \ _ [in SetPairFunIndPred]
_ :u: _ [in SetPairFunIndPred]
_ /c= _ [in SetPairFunIndPred]
_ c= _ [in SetPairFunIndPred]
_ /:e _ [in SetPairFunIndPred]
_ :e _ [in SetPairFunIndPred]
_ <> _ [in SetPairFunIndPred]
_ = _ [in SetPairFunIndPred]
_ <-> _ [in SetPairFunIndPred]
_ \/ _ [in SetPairFunIndPred]
_ /\ _ [in SetPairFunIndPred]
existsf _ , _ [in SetPairFunKT]
existsf _ , _ [in SetPairFun]
existsf _ , _ [in SetPairFunIndPred]
exists! _ , _ [in SetPairFunKT]
exists! _ , _ [in SetPairFun]
exists! _ , _ [in SetPairFunIndPred]
exists _ , _ [in SetPairFunKT]
exists _ , _ [in SetPairFun]
exists _ , _ [in SetPairFunIndPred]
U _ : _ , _ [in SetPairFunKT]
U _ : _ , _ [in SetPairFun]
U _ : _ , _ [in SetPairFunIndPred]
0 [in SetPairFunKT]
0 [in SetPairFun]
0 [in SetPairFunIndPred]
1 [in SetPairFunKT]
1 [in SetPairFun]
1 [in SetPairFunIndPred]
2 [in SetPairFunKT]
2 [in SetPairFun]
2 [in SetPairFunIndPred]
{ _ , _ } [in SetPairFunKT]
{ _ | _ :i _ } [in SetPairFunKT]
{ _ :i _ | _ } [in SetPairFunKT]
{ _ , _ } [in SetPairFun]
{ _ | _ :i _ } [in SetPairFun]
{ _ :i _ | _ } [in SetPairFun]
{ _ , _ } [in SetPairFunIndPred]
{ _ | _ :i _ } [in SetPairFunIndPred]
{ _ :i _ | _ } [in SetPairFunIndPred]
{| _ |} [in SetPairFunKT]
{| _ |} [in SetPairFun]
{| _ |} [in SetPairFunIndPred]
~ _ [in SetPairFunKT]
~ _ [in SetPairFun]
~ _ [in SetPairFunIndPred]
Module Index
P
PairFun [in SetPairFunKT]PairFun [in SetPairFun]
PairFun [in SetPairFunIndPred]
PairFunConseq [in SetPairFunKT]
PairFunConseq [in SetPairFun]
PairFunConseq [in SetPairFunIndPred]
PairFunImpl [in SetPairFunKT]
PairFunImpl [in SetPairFun]
PairFunImpl [in SetPairFunIndPred]
Variable Index
E
EpsilonRec.Phi [in SetPairFunKT]EpsilonRec.Phi [in SetPairFun]
EpsilonRec.Phi [in SetPairFunIndPred]
EpsilonRec.Phir [in SetPairFunKT]
EpsilonRec.Phir [in SetPairFun]
EpsilonRec.Phir [in SetPairFunIndPred]
EpsilonRec.Psi [in SetPairFunKT]
K
KnasterTarski.Psi [in SetPairFunKT]KnasterTarski.Psim [in SetPairFunKT]
Library Index
S
SetPairFunSetPairFunIndPred
SetPairFunKT
Lemma Index
A
andI [in SetPairFunKT]andI [in SetPairFun]
andI [in SetPairFunIndPred]
B
binunionE [in SetPairFunKT]binunionE [in SetPairFun]
binunionE [in SetPairFunIndPred]
binunionEq [in SetPairFunKT]
binunionEq [in SetPairFun]
binunionEq [in SetPairFunIndPred]
binunionI1 [in SetPairFunKT]
binunionI1 [in SetPairFun]
binunionI1 [in SetPairFunIndPred]
binunionI2 [in SetPairFunKT]
binunionI2 [in SetPairFun]
binunionI2 [in SetPairFunIndPred]
E
EmptyE [in SetPairFunKT]EmptyE [in SetPairFun]
EmptyE [in SetPairFunIndPred]
Empty_Power [in SetPairFunKT]
Empty_Power [in SetPairFun]
Empty_Power [in SetPairFunIndPred]
eqI [in SetPairFunKT]
eqI [in SetPairFun]
eqI [in SetPairFunIndPred]
eq_2_Sing0 [in SetPairFunKT]
eq_1_Sing0 [in SetPairFunKT]
eq_sym [in SetPairFunKT]
eq_2_Sing0 [in SetPairFun]
eq_1_Sing0 [in SetPairFun]
eq_sym [in SetPairFun]
eq_2_Sing0 [in SetPairFunIndPred]
eq_1_Sing0 [in SetPairFunIndPred]
eq_sym [in SetPairFunIndPred]
exI [in SetPairFunKT]
exI [in SetPairFun]
exI [in SetPairFunIndPred]
exI_f [in SetPairFunKT]
exI_f [in SetPairFun]
exI_f [in SetPairFunIndPred]
exuI [in SetPairFunKT]
exuI [in SetPairFun]
exuI [in SetPairFunIndPred]
F
famunionE [in SetPairFunKT]famunionE [in SetPairFun]
famunionE [in SetPairFunIndPred]
famunionEq [in SetPairFunKT]
famunionEq [in SetPairFun]
famunionEq [in SetPairFunIndPred]
famunionI [in SetPairFunKT]
famunionI [in SetPairFun]
famunionI [in SetPairFunIndPred]
I
iffI [in SetPairFunKT]iffI [in SetPairFun]
iffI [in SetPairFunIndPred]
In_rec_eq [in SetPairFunKT]
In_rec_G_In_rec_d [in SetPairFunKT]
In_rec_G_In_rec [in SetPairFunKT]
In_rec_G_f [in SetPairFunKT]
In_rec_G_c [in SetPairFunKT]
in_2_Eq [in SetPairFunKT]
in_2_E [in SetPairFunKT]
in_1_Eq [in SetPairFunKT]
in_1_E [in SetPairFunKT]
in_1_2 [in SetPairFunKT]
in_0_2 [in SetPairFunKT]
in_0_1 [in SetPairFunKT]
In_Power [in SetPairFunKT]
In_rec_eq [in SetPairFun]
In_rec_G_In_rec_d [in SetPairFun]
In_rec_G_In_rec [in SetPairFun]
In_rec_G_f [in SetPairFun]
In_rec_G_inv [in SetPairFun]
In_rec_G_ind [in SetPairFun]
In_rec_G_c [in SetPairFun]
in_2_Eq [in SetPairFun]
in_2_E [in SetPairFun]
in_1_Eq [in SetPairFun]
in_1_E [in SetPairFun]
in_1_2 [in SetPairFun]
in_0_2 [in SetPairFun]
in_0_1 [in SetPairFun]
In_Power [in SetPairFun]
In_rec_eq [in SetPairFunIndPred]
In_rec_G_In_rec_d [in SetPairFunIndPred]
In_rec_G_In_rec [in SetPairFunIndPred]
In_rec_G_f [in SetPairFunIndPred]
In_rec_G_inv [in SetPairFunIndPred]
in_2_Eq [in SetPairFunIndPred]
in_2_E [in SetPairFunIndPred]
in_1_Eq [in SetPairFunIndPred]
in_1_E [in SetPairFunIndPred]
in_1_2 [in SetPairFunIndPred]
in_0_2 [in SetPairFunIndPred]
in_0_1 [in SetPairFunIndPred]
In_Power [in SetPairFunIndPred]
L
lfp_eq [in SetPairFunKT]lfp_post [in SetPairFunKT]
lfp_pre [in SetPairFunKT]
N
nat_in_dec [in SetPairFunKT]nat_ordsucc_in_ordsucc [in SetPairFunKT]
nat_trans [in SetPairFunKT]
nat_in_nat [in SetPairFunKT]
nat_0_in_ordsucc [in SetPairFunKT]
nat_complete_ind [in SetPairFunKT]
nat_inv [in SetPairFunKT]
nat_ind [in SetPairFunKT]
nat_2 [in SetPairFunKT]
nat_1 [in SetPairFunKT]
nat_ordsucc [in SetPairFunKT]
nat_0 [in SetPairFunKT]
nat_in_dec [in SetPairFun]
nat_ordsucc_in_ordsucc [in SetPairFun]
nat_trans [in SetPairFun]
nat_in_nat [in SetPairFun]
nat_0_in_ordsucc [in SetPairFun]
nat_complete_ind [in SetPairFun]
nat_inv [in SetPairFun]
nat_ind [in SetPairFun]
nat_2 [in SetPairFun]
nat_1 [in SetPairFun]
nat_ordsucc [in SetPairFun]
nat_0 [in SetPairFun]
nat_in_dec [in SetPairFunIndPred]
nat_ordsucc_in_ordsucc [in SetPairFunIndPred]
nat_trans [in SetPairFunIndPred]
nat_in_nat [in SetPairFunIndPred]
nat_0_in_ordsucc [in SetPairFunIndPred]
nat_complete_ind [in SetPairFunIndPred]
nat_inv [in SetPairFunIndPred]
nat_ind [in SetPairFunIndPred]
nat_2 [in SetPairFunIndPred]
nat_1 [in SetPairFunIndPred]
nat_ordsucc [in SetPairFunIndPred]
nat_0 [in SetPairFunIndPred]
neq_0_1 [in SetPairFunKT]
neq_0_1 [in SetPairFun]
neq_0_1 [in SetPairFunIndPred]
O
ordsuccE [in SetPairFunKT]ordsuccE [in SetPairFun]
ordsuccE [in SetPairFunIndPred]
ordsucc_in [in SetPairFunKT]
ordsucc_Subq [in SetPairFunKT]
ordsucc_in [in SetPairFun]
ordsucc_Subq [in SetPairFun]
ordsucc_in [in SetPairFunIndPred]
ordsucc_Subq [in SetPairFunIndPred]
orIL [in SetPairFunKT]
orIL [in SetPairFun]
orIL [in SetPairFunIndPred]
orIR [in SetPairFunKT]
orIR [in SetPairFun]
orIR [in SetPairFunIndPred]
P
PairFunConseq.ap0_Sigma [in SetPairFunKT]PairFunConseq.ap0_Sigma [in SetPairFun]
PairFunConseq.ap0_Sigma [in SetPairFunIndPred]
PairFunConseq.ap1_Sigma [in SetPairFunKT]
PairFunConseq.ap1_Sigma [in SetPairFun]
PairFunConseq.ap1_Sigma [in SetPairFunIndPred]
PairFunConseq.pair_ap_n2 [in SetPairFunKT]
PairFunConseq.pair_ap_1 [in SetPairFunKT]
PairFunConseq.pair_ap_0 [in SetPairFunKT]
PairFunConseq.pair_lam2_ex [in SetPairFunKT]
PairFunConseq.pair_ap_n2 [in SetPairFun]
PairFunConseq.pair_ap_1 [in SetPairFun]
PairFunConseq.pair_ap_0 [in SetPairFun]
PairFunConseq.pair_lam2_ex [in SetPairFun]
PairFunConseq.pair_ap_n2 [in SetPairFunIndPred]
PairFunConseq.pair_ap_1 [in SetPairFunIndPred]
PairFunConseq.pair_ap_0 [in SetPairFunIndPred]
PairFunConseq.pair_lam2_ex [in SetPairFunIndPred]
PairFunConseq.setexp_2_eq [in SetPairFunKT]
PairFunConseq.setexp_2_eq [in SetPairFun]
PairFunConseq.setexp_2_eq [in SetPairFunIndPred]
PairFunImpl.apE [in SetPairFunKT]
PairFunImpl.apE [in SetPairFun]
PairFunImpl.apE [in SetPairFunIndPred]
PairFunImpl.apEq [in SetPairFunKT]
PairFunImpl.apEq [in SetPairFun]
PairFunImpl.apEq [in SetPairFunIndPred]
PairFunImpl.apI [in SetPairFunKT]
PairFunImpl.apI [in SetPairFun]
PairFunImpl.apI [in SetPairFunIndPred]
PairFunImpl.ap_Pi [in SetPairFunKT]
PairFunImpl.ap_Pi [in SetPairFun]
PairFunImpl.ap_Pi [in SetPairFunIndPred]
PairFunImpl.ap0_Sigma [in SetPairFunKT]
PairFunImpl.ap0_Sigma [in SetPairFun]
PairFunImpl.ap0_Sigma [in SetPairFunIndPred]
PairFunImpl.ap1_Sigma [in SetPairFunKT]
PairFunImpl.ap1_Sigma [in SetPairFun]
PairFunImpl.ap1_Sigma [in SetPairFunIndPred]
PairFunImpl.beta [in SetPairFunKT]
PairFunImpl.beta [in SetPairFun]
PairFunImpl.beta [in SetPairFunIndPred]
PairFunImpl.beta0 [in SetPairFunKT]
PairFunImpl.beta0 [in SetPairFun]
PairFunImpl.beta0 [in SetPairFunIndPred]
PairFunImpl.Inj0E [in SetPairFunKT]
PairFunImpl.Inj0E [in SetPairFun]
PairFunImpl.Inj0E [in SetPairFunIndPred]
PairFunImpl.Inj0I [in SetPairFunKT]
PairFunImpl.Inj0I [in SetPairFun]
PairFunImpl.Inj0I [in SetPairFunIndPred]
PairFunImpl.Inj0_0 [in SetPairFunKT]
PairFunImpl.Inj0_Inj1_neq [in SetPairFunKT]
PairFunImpl.Inj0_inj [in SetPairFunKT]
PairFunImpl.Inj0_0 [in SetPairFun]
PairFunImpl.Inj0_Inj1_neq [in SetPairFun]
PairFunImpl.Inj0_inj [in SetPairFun]
PairFunImpl.Inj0_0 [in SetPairFunIndPred]
PairFunImpl.Inj0_Inj1_neq [in SetPairFunIndPred]
PairFunImpl.Inj0_inj [in SetPairFunIndPred]
PairFunImpl.Inj1E [in SetPairFunKT]
PairFunImpl.Inj1E [in SetPairFun]
PairFunImpl.Inj1E [in SetPairFunIndPred]
PairFunImpl.Inj1I1 [in SetPairFunKT]
PairFunImpl.Inj1I1 [in SetPairFun]
PairFunImpl.Inj1I1 [in SetPairFunIndPred]
PairFunImpl.Inj1I2 [in SetPairFunKT]
PairFunImpl.Inj1I2 [in SetPairFun]
PairFunImpl.Inj1I2 [in SetPairFunIndPred]
PairFunImpl.Inj1_inj [in SetPairFunKT]
PairFunImpl.Inj1_eq [in SetPairFunKT]
PairFunImpl.Inj1_inj [in SetPairFun]
PairFunImpl.Inj1_eq [in SetPairFun]
PairFunImpl.Inj1_inj [in SetPairFunIndPred]
PairFunImpl.Inj1_eq [in SetPairFunIndPred]
PairFunImpl.lamE [in SetPairFunKT]
PairFunImpl.lamE [in SetPairFun]
PairFunImpl.lamE [in SetPairFunIndPred]
PairFunImpl.lamEq [in SetPairFunKT]
PairFunImpl.lamEq [in SetPairFun]
PairFunImpl.lamEq [in SetPairFunIndPred]
PairFunImpl.lamI [in SetPairFunKT]
PairFunImpl.lamI [in SetPairFun]
PairFunImpl.lamI [in SetPairFunIndPred]
PairFunImpl.lamPE [in SetPairFunKT]
PairFunImpl.lamPE [in SetPairFun]
PairFunImpl.lamPE [in SetPairFunIndPred]
PairFunImpl.lamPEq [in SetPairFunKT]
PairFunImpl.lamPEq [in SetPairFun]
PairFunImpl.lamPEq [in SetPairFunIndPred]
PairFunImpl.lam_PiEq [in SetPairFunKT]
PairFunImpl.lam_PiE [in SetPairFunKT]
PairFunImpl.lam_PiI [in SetPairFunKT]
PairFunImpl.lam_spec [in SetPairFunKT]
PairFunImpl.lam_inj [in SetPairFunKT]
PairFunImpl.lam_inj_lem [in SetPairFunKT]
PairFunImpl.lam_PiEq [in SetPairFun]
PairFunImpl.lam_PiE [in SetPairFun]
PairFunImpl.lam_PiI [in SetPairFun]
PairFunImpl.lam_spec [in SetPairFun]
PairFunImpl.lam_inj [in SetPairFun]
PairFunImpl.lam_inj_lem [in SetPairFun]
PairFunImpl.lam_PiEq [in SetPairFunIndPred]
PairFunImpl.lam_PiE [in SetPairFunIndPred]
PairFunImpl.lam_PiI [in SetPairFunIndPred]
PairFunImpl.lam_spec [in SetPairFunIndPred]
PairFunImpl.lam_inj [in SetPairFunIndPred]
PairFunImpl.lam_inj_lem [in SetPairFunIndPred]
PairFunImpl.lam2_pair [in SetPairFunKT]
PairFunImpl.lam2_pair [in SetPairFun]
PairFunImpl.lam2_pair [in SetPairFunIndPred]
PairFunImpl.nat_sum1_ordsucc [in SetPairFunKT]
PairFunImpl.nat_pair1_ordsucc [in SetPairFunKT]
PairFunImpl.nat_in_setexp_mon [in SetPairFunKT]
PairFunImpl.nat_sum1_ordsucc [in SetPairFun]
PairFunImpl.nat_pair1_ordsucc [in SetPairFun]
PairFunImpl.nat_in_setexp_mon [in SetPairFun]
PairFunImpl.nat_sum1_ordsucc [in SetPairFunIndPred]
PairFunImpl.nat_pair1_ordsucc [in SetPairFunIndPred]
PairFunImpl.nat_in_setexp_mon [in SetPairFunIndPred]
PairFunImpl.pairE [in SetPairFunKT]
PairFunImpl.pairE [in SetPairFun]
PairFunImpl.pairE [in SetPairFunIndPred]
PairFunImpl.pairEq [in SetPairFunKT]
PairFunImpl.pairEq [in SetPairFun]
PairFunImpl.pairEq [in SetPairFunIndPred]
PairFunImpl.pairE0 [in SetPairFunKT]
PairFunImpl.pairE0 [in SetPairFun]
PairFunImpl.pairE0 [in SetPairFunIndPred]
PairFunImpl.pairE1 [in SetPairFunKT]
PairFunImpl.pairE1 [in SetPairFun]
PairFunImpl.pairE1 [in SetPairFunIndPred]
PairFunImpl.pairI0 [in SetPairFunKT]
PairFunImpl.pairI0 [in SetPairFun]
PairFunImpl.pairI0 [in SetPairFunIndPred]
PairFunImpl.pairI1 [in SetPairFunKT]
PairFunImpl.pairI1 [in SetPairFun]
PairFunImpl.pairI1 [in SetPairFunIndPred]
PairFunImpl.pairSubq [in SetPairFunKT]
PairFunImpl.pairSubq [in SetPairFun]
PairFunImpl.pairSubq [in SetPairFunIndPred]
PairFunImpl.pair_1_1_2 [in SetPairFunKT]
PairFunImpl.pair_1_0_1 [in SetPairFunKT]
PairFunImpl.pair_SigmaEq [in SetPairFunKT]
PairFunImpl.pair_SigmaE [in SetPairFunKT]
PairFunImpl.pair_SigmaI [in SetPairFunKT]
PairFunImpl.pair_ap_n2 [in SetPairFunKT]
PairFunImpl.pair_ap_1 [in SetPairFunKT]
PairFunImpl.pair_ap_0 [in SetPairFunKT]
PairFunImpl.pair_spec [in SetPairFunKT]
PairFunImpl.pair_inj [in SetPairFunKT]
PairFunImpl.pair_inj_Subq_1 [in SetPairFunKT]
PairFunImpl.pair_inj_Subq_0 [in SetPairFunKT]
PairFunImpl.pair_0_1_neq [in SetPairFunKT]
PairFunImpl.pair_1_inj [in SetPairFunKT]
PairFunImpl.pair_0_inj [in SetPairFunKT]
PairFunImpl.pair_1_x [in SetPairFunKT]
PairFunImpl.pair_0_x [in SetPairFunKT]
PairFunImpl.pair_0_0 [in SetPairFunKT]
PairFunImpl.pair_1_1_2 [in SetPairFun]
PairFunImpl.pair_1_0_1 [in SetPairFun]
PairFunImpl.pair_SigmaEq [in SetPairFun]
PairFunImpl.pair_SigmaE [in SetPairFun]
PairFunImpl.pair_SigmaI [in SetPairFun]
PairFunImpl.pair_ap_n2 [in SetPairFun]
PairFunImpl.pair_ap_1 [in SetPairFun]
PairFunImpl.pair_ap_0 [in SetPairFun]
PairFunImpl.pair_spec [in SetPairFun]
PairFunImpl.pair_inj [in SetPairFun]
PairFunImpl.pair_inj_Subq_1 [in SetPairFun]
PairFunImpl.pair_inj_Subq_0 [in SetPairFun]
PairFunImpl.pair_0_1_neq [in SetPairFun]
PairFunImpl.pair_1_inj [in SetPairFun]
PairFunImpl.pair_0_inj [in SetPairFun]
PairFunImpl.pair_1_x [in SetPairFun]
PairFunImpl.pair_0_x [in SetPairFun]
PairFunImpl.pair_0_0 [in SetPairFun]
PairFunImpl.pair_1_1_2 [in SetPairFunIndPred]
PairFunImpl.pair_1_0_1 [in SetPairFunIndPred]
PairFunImpl.pair_SigmaEq [in SetPairFunIndPred]
PairFunImpl.pair_SigmaE [in SetPairFunIndPred]
PairFunImpl.pair_SigmaI [in SetPairFunIndPred]
PairFunImpl.pair_ap_n2 [in SetPairFunIndPred]
PairFunImpl.pair_ap_1 [in SetPairFunIndPred]
PairFunImpl.pair_ap_0 [in SetPairFunIndPred]
PairFunImpl.pair_spec [in SetPairFunIndPred]
PairFunImpl.pair_inj [in SetPairFunIndPred]
PairFunImpl.pair_inj_Subq_1 [in SetPairFunIndPred]
PairFunImpl.pair_inj_Subq_0 [in SetPairFunIndPred]
PairFunImpl.pair_0_1_neq [in SetPairFunIndPred]
PairFunImpl.pair_1_inj [in SetPairFunIndPred]
PairFunImpl.pair_0_inj [in SetPairFunIndPred]
PairFunImpl.pair_1_x [in SetPairFunIndPred]
PairFunImpl.pair_0_x [in SetPairFunIndPred]
PairFunImpl.pair_0_0 [in SetPairFunIndPred]
PairFunImpl.pair0_sum [in SetPairFunKT]
PairFunImpl.pair0_sum [in SetPairFun]
PairFunImpl.pair0_sum [in SetPairFunIndPred]
PairFunImpl.pair1_sum [in SetPairFunKT]
PairFunImpl.pair1_sum [in SetPairFun]
PairFunImpl.pair1_sum [in SetPairFunIndPred]
PairFunImpl.Pi_0_mon [in SetPairFunKT]
PairFunImpl.Pi_cod_mon [in SetPairFunKT]
PairFunImpl.Pi_0_dom_mon [in SetPairFunKT]
PairFunImpl.Pi_Power_1 [in SetPairFunKT]
PairFunImpl.Pi_eta [in SetPairFunKT]
PairFunImpl.Pi_0_mon [in SetPairFun]
PairFunImpl.Pi_cod_mon [in SetPairFun]
PairFunImpl.Pi_0_dom_mon [in SetPairFun]
PairFunImpl.Pi_Power_1 [in SetPairFun]
PairFunImpl.Pi_eta [in SetPairFun]
PairFunImpl.Pi_0_mon [in SetPairFunIndPred]
PairFunImpl.Pi_cod_mon [in SetPairFunIndPred]
PairFunImpl.Pi_0_dom_mon [in SetPairFunIndPred]
PairFunImpl.Pi_Power_1 [in SetPairFunIndPred]
PairFunImpl.Pi_eta [in SetPairFunIndPred]
PairFunImpl.setexp_0_mon [in SetPairFunKT]
PairFunImpl.setexp_0_dom_mon [in SetPairFunKT]
PairFunImpl.setexp_2_eq [in SetPairFunKT]
PairFunImpl.setexp_0_mon [in SetPairFun]
PairFunImpl.setexp_0_dom_mon [in SetPairFun]
PairFunImpl.setexp_2_eq [in SetPairFun]
PairFunImpl.setexp_0_mon [in SetPairFunIndPred]
PairFunImpl.setexp_0_dom_mon [in SetPairFunIndPred]
PairFunImpl.setexp_2_eq [in SetPairFunIndPred]
PairFunImpl.Sigma_mon1 [in SetPairFunKT]
PairFunImpl.Sigma_mon0 [in SetPairFunKT]
PairFunImpl.Sigma_mon [in SetPairFunKT]
PairFunImpl.Sigma_Power_1 [in SetPairFunKT]
PairFunImpl.Sigma_eta [in SetPairFunKT]
PairFunImpl.Sigma_mon1 [in SetPairFun]
PairFunImpl.Sigma_mon0 [in SetPairFun]
PairFunImpl.Sigma_mon [in SetPairFun]
PairFunImpl.Sigma_Power_1 [in SetPairFun]
PairFunImpl.Sigma_eta [in SetPairFun]
PairFunImpl.Sigma_mon1 [in SetPairFunIndPred]
PairFunImpl.Sigma_mon0 [in SetPairFunIndPred]
PairFunImpl.Sigma_mon [in SetPairFunIndPred]
PairFunImpl.Sigma_Power_1 [in SetPairFunIndPred]
PairFunImpl.Sigma_eta [in SetPairFunIndPred]
PairFunImpl.sumEq [in SetPairFunKT]
PairFunImpl.sumEq [in SetPairFun]
PairFunImpl.sumEq [in SetPairFunIndPred]
PairFunImpl.sum_mon [in SetPairFunKT]
PairFunImpl.sum_1_1_2 [in SetPairFunKT]
PairFunImpl.sum_1_0_1 [in SetPairFunKT]
PairFunImpl.sum_inv [in SetPairFunKT]
PairFunImpl.sum_mon [in SetPairFun]
PairFunImpl.sum_1_1_2 [in SetPairFun]
PairFunImpl.sum_1_0_1 [in SetPairFun]
PairFunImpl.sum_inv [in SetPairFun]
PairFunImpl.sum_mon [in SetPairFunIndPred]
PairFunImpl.sum_1_1_2 [in SetPairFunIndPred]
PairFunImpl.sum_1_0_1 [in SetPairFunIndPred]
PairFunImpl.sum_inv [in SetPairFunIndPred]
PairFunImpl.Unj_Inj0_eq [in SetPairFunKT]
PairFunImpl.Unj_Inj1_eq [in SetPairFunKT]
PairFunImpl.Unj_eq [in SetPairFunKT]
PairFunImpl.Unj_Inj0_eq [in SetPairFun]
PairFunImpl.Unj_Inj1_eq [in SetPairFun]
PairFunImpl.Unj_eq [in SetPairFun]
PairFunImpl.Unj_Inj0_eq [in SetPairFunIndPred]
PairFunImpl.Unj_Inj1_eq [in SetPairFunIndPred]
PairFunImpl.Unj_eq [in SetPairFunIndPred]
PhiPsim [in SetPairFunKT]
PowerE [in SetPairFunKT]
PowerE [in SetPairFun]
PowerE [in SetPairFunIndPred]
PowerI [in SetPairFunKT]
PowerI [in SetPairFun]
PowerI [in SetPairFunIndPred]
R
ReplE [in SetPairFunKT]ReplE [in SetPairFun]
ReplE [in SetPairFunIndPred]
ReplI [in SetPairFunKT]
ReplI [in SetPairFun]
ReplI [in SetPairFunIndPred]
Repl_Empty [in SetPairFunKT]
Repl_restr [in SetPairFunKT]
Repl_restr_1 [in SetPairFunKT]
Repl_Empty [in SetPairFun]
Repl_restr [in SetPairFun]
Repl_restr_1 [in SetPairFun]
Repl_Empty [in SetPairFunIndPred]
Repl_restr [in SetPairFunIndPred]
Repl_restr_1 [in SetPairFunIndPred]
S
SepE [in SetPairFunKT]SepE [in SetPairFun]
SepE [in SetPairFunIndPred]
SepE1 [in SetPairFunKT]
SepE1 [in SetPairFun]
SepE1 [in SetPairFunIndPred]
SepE2 [in SetPairFunKT]
SepE2 [in SetPairFun]
SepE2 [in SetPairFunIndPred]
SepI [in SetPairFunKT]
SepI [in SetPairFun]
SepI [in SetPairFunIndPred]
setminusEq [in SetPairFunKT]
setminusEq [in SetPairFun]
setminusEq [in SetPairFunIndPred]
setminusE1 [in SetPairFunKT]
setminusE1 [in SetPairFun]
setminusE1 [in SetPairFunIndPred]
setminusE2 [in SetPairFunKT]
setminusE2 [in SetPairFun]
setminusE2 [in SetPairFunIndPred]
setminusI [in SetPairFunKT]
setminusI [in SetPairFun]
setminusI [in SetPairFunIndPred]
SingE [in SetPairFunKT]
SingE [in SetPairFun]
SingE [in SetPairFunIndPred]
SingEq [in SetPairFunKT]
SingEq [in SetPairFun]
SingEq [in SetPairFunIndPred]
SingI [in SetPairFunKT]
SingI [in SetPairFun]
SingI [in SetPairFunIndPred]
Subq_Empty [in SetPairFunKT]
Subq_tra [in SetPairFunKT]
Subq_ref [in SetPairFunKT]
Subq_Empty [in SetPairFun]
Subq_tra [in SetPairFun]
Subq_ref [in SetPairFun]
Subq_Empty [in SetPairFunIndPred]
Subq_tra [in SetPairFunIndPred]
Subq_ref [in SetPairFunIndPred]
U
UnionE [in SetPairFunKT]UnionE [in SetPairFun]
UnionE [in SetPairFunIndPred]
UnionI [in SetPairFunKT]
UnionI [in SetPairFun]
UnionI [in SetPairFunIndPred]
UPairE [in SetPairFunKT]
UPairE [in SetPairFun]
UPairE [in SetPairFunIndPred]
UPairEq [in SetPairFunKT]
UPairEq [in SetPairFun]
UPairEq [in SetPairFunIndPred]
UPairI1 [in SetPairFunKT]
UPairI1 [in SetPairFun]
UPairI1 [in SetPairFunIndPred]
UPairI2 [in SetPairFunKT]
UPairI2 [in SetPairFun]
UPairI2 [in SetPairFunIndPred]
Axiom Index
D
Descr [in SetPairFunKT]Descr [in SetPairFun]
Descr [in SetPairFunIndPred]
DescrR [in SetPairFunKT]
DescrR [in SetPairFun]
DescrR [in SetPairFunIndPred]
E
Empty [in SetPairFunKT]Empty [in SetPairFun]
Empty [in SetPairFunIndPred]
EmptyAx [in SetPairFunKT]
EmptyAx [in SetPairFun]
EmptyAx [in SetPairFunIndPred]
I
In [in SetPairFunKT]In [in SetPairFun]
In [in SetPairFunIndPred]
In_ind [in SetPairFunKT]
In_ind [in SetPairFun]
In_ind [in SetPairFunIndPred]
P
PairFun.ap [in SetPairFunKT]PairFun.ap [in SetPairFun]
PairFun.ap [in SetPairFunIndPred]
PairFun.ap_Pi [in SetPairFunKT]
PairFun.ap_Pi [in SetPairFun]
PairFun.ap_Pi [in SetPairFunIndPred]
PairFun.beta [in SetPairFunKT]
PairFun.beta [in SetPairFun]
PairFun.beta [in SetPairFunIndPred]
PairFun.beta0 [in SetPairFunKT]
PairFun.beta0 [in SetPairFun]
PairFun.beta0 [in SetPairFunIndPred]
PairFun.lam [in SetPairFunKT]
PairFun.lam [in SetPairFun]
PairFun.lam [in SetPairFunIndPred]
PairFun.lam_PiEq [in SetPairFunKT]
PairFun.lam_spec [in SetPairFunKT]
PairFun.lam_PiEq [in SetPairFun]
PairFun.lam_spec [in SetPairFun]
PairFun.lam_PiEq [in SetPairFunIndPred]
PairFun.lam_spec [in SetPairFunIndPred]
PairFun.lam2_pair [in SetPairFunKT]
PairFun.lam2_pair [in SetPairFun]
PairFun.lam2_pair [in SetPairFunIndPred]
PairFun.pair [in SetPairFunKT]
PairFun.pair [in SetPairFun]
PairFun.pair [in SetPairFunIndPred]
PairFun.pair_SigmaEq [in SetPairFunKT]
PairFun.pair_spec [in SetPairFunKT]
PairFun.pair_SigmaEq [in SetPairFun]
PairFun.pair_spec [in SetPairFun]
PairFun.pair_SigmaEq [in SetPairFunIndPred]
PairFun.pair_spec [in SetPairFunIndPred]
PairFun.PI [in SetPairFunKT]
PairFun.PI [in SetPairFun]
PairFun.PI [in SetPairFunIndPred]
PairFun.Pi_Power_1 [in SetPairFunKT]
PairFun.Pi_Power_1 [in SetPairFun]
PairFun.Pi_Power_1 [in SetPairFunIndPred]
PairFun.SIGMA [in SetPairFunKT]
PairFun.SIGMA [in SetPairFun]
PairFun.SIGMA [in SetPairFunIndPred]
PairFun.Sigma_Power_1 [in SetPairFunKT]
PairFun.Sigma_Power_1 [in SetPairFun]
PairFun.Sigma_Power_1 [in SetPairFunIndPred]
Power [in SetPairFunKT]
Power [in SetPairFun]
Power [in SetPairFunIndPred]
PowerEq [in SetPairFunKT]
PowerEq [in SetPairFun]
PowerEq [in SetPairFunIndPred]
R
Repl [in SetPairFunKT]Repl [in SetPairFun]
Repl [in SetPairFunIndPred]
ReplEq [in SetPairFunKT]
ReplEq [in SetPairFun]
ReplEq [in SetPairFunIndPred]
S
Sep [in SetPairFunKT]Sep [in SetPairFun]
Sep [in SetPairFunIndPred]
SepEq [in SetPairFunKT]
SepEq [in SetPairFun]
SepEq [in SetPairFunIndPred]
set [in SetPairFunKT]
set [in SetPairFun]
set [in SetPairFunIndPred]
set_ext [in SetPairFunKT]
set_ext [in SetPairFun]
set_ext [in SetPairFunIndPred]
U
Union [in SetPairFunKT]Union [in SetPairFun]
Union [in SetPairFunIndPred]
UnionEq [in SetPairFunKT]
UnionEq [in SetPairFun]
UnionEq [in SetPairFunIndPred]
Constructor Index
I
In_rec_G_c [in SetPairFunIndPred]Inductive Index
I
In_rec_G [in SetPairFunIndPred]Section Index
E
EpsilonRec [in SetPairFunKT]EpsilonRec [in SetPairFun]
EpsilonRec [in SetPairFunIndPred]
K
KnasterTarski [in SetPairFunKT]Definition Index
A
and [in SetPairFunKT]and [in SetPairFun]
and [in SetPairFunIndPred]
B
binunion [in SetPairFunKT]binunion [in SetPairFun]
binunion [in SetPairFunIndPred]
C
Cond_Phi [in SetPairFunKT]Cond_Phi [in SetPairFun]
Cond_Phi [in SetPairFunIndPred]
E
eq [in SetPairFunKT]eq [in SetPairFun]
eq [in SetPairFunIndPred]
ex [in SetPairFunKT]
ex [in SetPairFun]
ex [in SetPairFunIndPred]
exu [in SetPairFunKT]
exu [in SetPairFun]
exu [in SetPairFunIndPred]
ex_f [in SetPairFunKT]
ex_f [in SetPairFun]
ex_f [in SetPairFunIndPred]
F
False [in SetPairFunKT]False [in SetPairFun]
False [in SetPairFunIndPred]
famunion [in SetPairFunKT]
famunion [in SetPairFun]
famunion [in SetPairFunIndPred]
I
iff [in SetPairFunKT]iff [in SetPairFun]
iff [in SetPairFunIndPred]
In_rec [in SetPairFunKT]
In_rec_G [in SetPairFunKT]
In_rec [in SetPairFun]
In_rec_G [in SetPairFun]
In_rec [in SetPairFunIndPred]
L
lfp [in SetPairFunKT]N
nat_p [in SetPairFunKT]nat_p [in SetPairFun]
nat_p [in SetPairFunIndPred]
not [in SetPairFunKT]
not [in SetPairFun]
not [in SetPairFunIndPred]
O
or [in SetPairFunKT]or [in SetPairFun]
or [in SetPairFunIndPred]
ordsucc [in SetPairFunKT]
ordsucc [in SetPairFun]
ordsucc [in SetPairFunIndPred]
P
PairFunImpl.ap [in SetPairFunKT]PairFunImpl.ap [in SetPairFun]
PairFunImpl.ap [in SetPairFunIndPred]
PairFunImpl.Inj0 [in SetPairFunKT]
PairFunImpl.Inj0 [in SetPairFun]
PairFunImpl.Inj0 [in SetPairFunIndPred]
PairFunImpl.Inj1 [in SetPairFunKT]
PairFunImpl.Inj1 [in SetPairFun]
PairFunImpl.Inj1 [in SetPairFunIndPred]
PairFunImpl.lam [in SetPairFunKT]
PairFunImpl.lam [in SetPairFun]
PairFunImpl.lam [in SetPairFunIndPred]
PairFunImpl.pair [in SetPairFunKT]
PairFunImpl.pair [in SetPairFun]
PairFunImpl.pair [in SetPairFunIndPred]
PairFunImpl.PI [in SetPairFunKT]
PairFunImpl.PI [in SetPairFun]
PairFunImpl.PI [in SetPairFunIndPred]
PairFunImpl.SIGMA [in SetPairFunKT]
PairFunImpl.SIGMA [in SetPairFun]
PairFunImpl.SIGMA [in SetPairFunIndPred]
PairFunImpl.sum [in SetPairFunKT]
PairFunImpl.sum [in SetPairFun]
PairFunImpl.sum [in SetPairFunIndPred]
PairFunImpl.Unj [in SetPairFunKT]
PairFunImpl.Unj [in SetPairFun]
PairFunImpl.Unj [in SetPairFunIndPred]
Psi_monotone [in SetPairFunKT]
S
setminus [in SetPairFunKT]setminus [in SetPairFun]
setminus [in SetPairFunIndPred]
Sing [in SetPairFunKT]
Sing [in SetPairFun]
Sing [in SetPairFunIndPred]
Subq [in SetPairFunKT]
Subq [in SetPairFun]
Subq [in SetPairFunIndPred]
T
TSet [in SetPairFunKT]TSet [in SetPairFun]
TSet [in SetPairFunIndPred]
U
UPair [in SetPairFunKT]UPair [in SetPairFun]
UPair [in SetPairFunIndPred]
| 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 | (832 entries) |
| Notation 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 | (123 entries) |
| Module 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) |
| Variable 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) |
| 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 | (3 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 | (498 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 | (93 entries) |
| Constructor 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 | (1 entry) |
| Inductive 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 | (1 entry) |
| Section 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 | (4 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 | (91 entries) |
This page has been generated by coqdoc