Global Index

other

(5117 entries)

Instance Index

other

(301 entries)

Projection Index

other

(112 entries)

Record Index

other

(34 entries)

Lemma Index

other

(2407 entries)

Section Index

other

(126 entries)

Constructor Index

other

(207 entries)

Notation Index

other

(37 entries)

Abbreviation Index

other

(26 entries)

Inductive Index

other

(62 entries)

Definition Index

other

(953 entries)

Module Index

other

(139 entries)

Axiom Index

other

(187 entries)

Variable Index

other

(446 entries)

Library Index

other

(80 entries)

Global Index

A

B

C

D

E

F

G

H

I

K

K [definition, in Lambda]
kind [constructor, in TermECC]
kind [constructor, in Term]
KnasterTarski [section, in ZFfix]
KnasterTarski.A [variable, in ZFfix]
KnasterTarski.F [variable, in ZFfix]
KnasterTarski.Fmono [variable, in ZFfix]
KnasterTarski.Ftyp [variable, in ZFfix]
knaster_tarski [lemma, in ZFfix]
KSAT_intro [lemma, in Sat]

L

lam [definition, in ZFrelations]
Lam [module, in ZFlambda]
lam [definition, in HFrelation]
Lambda [library]
lam_ext [lemma, in HFrelation]
lam_is_function [lemma, in ZFrelations]
lam_rel [definition, in ZFrelations]
lam_is_func [lemma, in ZFrelations]
lam_domain [lemma, in HFrelation]
lam_elim [lemma, in HFrelation]
lam_rel_is_func [lemma, in ZFrelations]
lam_intro [lemma, in HFrelation]
Lam.Abs [definition, in ZFlambda]
Lam.Abs_typ [lemma, in ZFlambda]
Lam.Abs_typ0 [lemma, in ZFlambda]
Lam.App [definition, in ZFlambda]
Lam.App_typ [lemma, in ZFlambda]
Lam.App_typ0 [lemma, in ZFlambda]
Lam.Cst [definition, in ZFlambda]
Lam.Cst_typ0 [lemma, in ZFlambda]
Lam.Cst_typ [lemma, in ZFlambda]
Lam.Lambda [definition, in ZFlambda]
Lam.LambdaTerms [section, in ZFlambda]
Lam.LambdaTerms.A [variable, in ZFlambda]
Lam.Lambda_intro [lemma, in ZFlambda]
Lam.Lambda_ind [lemma, in ZFlambda]
Lam.Lambda_fix [lemma, in ZFlambda]
Lam.Lambda_elim [lemma, in ZFlambda]
Lam.Lambda_eqn [lemma, in ZFlambda]
Lam.LAMf [definition, in ZFlambda]
Lam.LAMf_morph [instance, in ZFlambda]
Lam.LAMf_mono [instance, in ZFlambda]
Lam.LAMf_ind [lemma, in ZFlambda]
Lam.Lamn [definition, in ZFlambda]
Lam.Lamn_case [lemma, in ZFlambda]
Lam.Lamn_incl_succ [lemma, in ZFlambda]
Lam.Lamn_incl [lemma, in ZFlambda]
Lam.Lamn_eq [lemma, in ZFlambda]
Lam.Var [definition, in ZFlambda]
Lam.Var_typ [lemma, in ZFlambda]
Lam.Var_typ0 [lemma, in ZFlambda]
Lc [module, in SN_NAT]
Lc [module, in SN_CC]
Lc [module, in GenRealSN]
Lc [module, in SN_CC_Real]
Lc [module, in GenModelSN]
Lc [module, in ObjectSN]
Lc [module, in SATnat]
LCeq [module, in Lambda]
LCeq.eq [definition, in Lambda]
LCeq.eq_equiv [definition, in Lambda]
LCeq.t [definition, in Lambda]
le [definition, in ZFnats]
le_refl [lemma, in ZFnats]
le_card_morph [instance, in ZFcard]
le_morph [instance, in ZFnats]
le_card_refl [instance, in ZFcard]
le_total [lemma, in ZFnats]
le_card [definition, in ZFcard]
le_card_trans [instance, in ZFcard]
le_lt_trans [lemma, in ZFord]
le_case [lemma, in ZFnats]
lfp_typ [lemma, in ZFfix]
lift [definition, in TermECC]
lift [definition, in Lambda]
lift [definition, in Term]
liftable [definition, in Lambda]
LiftAndSubstEquiv [section, in SN_CC_Real]
LiftAndSubstEquiv [section, in SN_CC]
lift_in [lemma, in EnsUniv]
lift_rec [definition, in TermECC]
lift_rec0 [lemma, in Term]
lift_ref_lt [lemma, in TermECC]
lift_rec0 [lemma, in TermECC]
lift_ref_ge [lemma, in Term]
lift_ref_lt [lemma, in Term]
lift_rec0 [lemma, in Lambda]
lift_rec [definition, in Term]
lift_ref_lt [lemma, in Lambda]
lift_rec [definition, in Lambda]
lift_ref_ge [lemma, in TermECC]
lift_closed [lemma, in Lambda]
lift_ref_ge [lemma, in Lambda]
lift_eq [lemma, in EnsUniv]
lift0 [lemma, in TermECC]
lift0 [lemma, in Term]
lift0 [lemma, in Lambda]
lim [definition, in ZFlimit]
Limit [section, in ZFlimit]
LimitMono [section, in ZFlimit]
LimitMono.F [variable, in ZFlimit]
LimitMono.Fext [variable, in ZFlimit]
LimitMono.Fmono [variable, in ZFlimit]
LimitMono.o [variable, in ZFlimit]
LimitMono.oord [variable, in ZFlimit]
LimitMono.os [variable, in ZFlimit]
limitOrd [definition, in ZFord]
LimitTI [section, in ZFlimit]
LimitTI.F [variable, in ZFlimit]
LimitTI.Fm [variable, in ZFlimit]
limit_union [lemma, in ZFord]
limit_is_ord [lemma, in ZFord]
limit_union_intro [lemma, in ZFord]
Limit.F [variable, in ZFlimit]
Limit.Fm [variable, in ZFlimit]
Limit.o [variable, in ZFlimit]
Limit.oord [variable, in ZFlimit]
LimOrd [section, in ZFord]
LimOrd.f [variable, in ZFord]
LimOrd.F [variable, in ZFord]
LimOrd.Fch [variable, in ZFord]
LimOrd.Fm [variable, in ZFord]
LimOrd.fmono [variable, in ZFord]
LimOrd.ford [variable, in ZFord]
lim_mono [lemma, in ZFlimit]
lim_ext [lemma, in ZFlimit]
lim_def_mono [lemma, in ZFlimit]
lim_def [lemma, in ZFlimit]
lim_morph [instance, in ZFlimit]
lim_cst [lemma, in ZFlimit]
lim_oucc [lemma, in ZFlimit]
List [definition, in ZFlist]
ListDefs [section, in ZFlist]
ListDefs.A [variable, in ZFlist]
Listes [section, in MyList]
Listes.A [variable, in MyList]
Listes.List [variable, in MyList]
LISTf [definition, in ZFlist]
LISTf_mono [instance, in ZFlist]
LISTf_morph [instance, in ZFlist]
LISTf_ind [lemma, in ZFlist]
List_mono [instance, in ZFlist]
LIST_case_Cons [lemma, in ZFlist]
List_elim [lemma, in ZFlist]
List_ind [lemma, in ZFlist]
List_intro [lemma, in ZFlist]
LIST_case [definition, in ZFlist]
LIST_case_Nil [lemma, in ZFlist]
List_eqn [lemma, in ZFlist]
List_morph [instance, in ZFlist]
list_item [lemma, in MyList]
List_fix [lemma, in ZFlist]
LIST_case_morph [instance, in ZFlist]
Lmono [lemma, in ZFind_wnup]
Lmorph [instance, in ZFind_wnup]
Logics [library]
lower_bound [lemma, in ZFfix]
Lstn [definition, in ZFlist]
Lstn_incl_succ [lemma, in ZFlist]
Lstn_case [lemma, in ZFlist]
Lstn_eq [lemma, in ZFlist]
Lstn_incl [lemma, in ZFlist]
lt [definition, in ZFnats]
lt_cardf [definition, in ZFrank]
lt_osucc_compat [lemma, in ZFord]
lt_mono [lemma, in ZFnats]
lt_antirefl [lemma, in ZFord]
lt_trans [lemma, in ZFnats]
lt_osucc_inv [lemma, in ZFord]
lt_morph [instance, in ZFnats]
lt_0_succ [lemma, in ZFnats]
lt_card [definition, in ZFcard]
lt_osucc [lemma, in ZFord]
lt_card_weaker [lemma, in ZFcard]
lt_card2 [definition, in ZFcard]
lt_is_le [lemma, in ZFnats]
L_elim [lemma, in ZFind_wnup]
L_intro2 [lemma, in ZFind_wnup]
L_match [definition, in ZFind_wnup]
L_intro1 [lemma, in ZFind_wnup]

M

N

O

ObjectSN [library]
occur [inductive, in Lambda]
occur_subst [lemma, in Lambda]
occ_app_r [constructor, in Lambda]
occ_var [constructor, in Lambda]
occ_abs [constructor, in Lambda]
occ_app_l [constructor, in Lambda]
oles_lt [lemma, in ZFord]
ole_lts [lemma, in ZFord]
olts_le [lemma, in ZFord]
omega [definition, in ZF]
omega [definition, in ZFord]
omega_in_omega [lemma, in ZF]
omega_limit_ord [lemma, in ZFord]
omega_not_in_omega [lemma, in ZF]
ONE [abbreviation, in HF]
one_step_conv_exp [lemma, in TermECC]
one_step_red [lemma, in Term]
one_step_red [lemma, in TermECC]
one_step_red [lemma, in Lambda]
one_step_conv_exp [lemma, in Term]
Ord [definition, in SN_CIC]
order_type_assign_rel_inv [lemma, in ZFcard]
order_type_assign_uchoice [lemma, in ZFcard]
order_type [definition, in ZFcard]
order_type_assign_ext [instance, in ZFcard]
order_type_assign_ord [lemma, in ZFcard]
order_type_assign_rel [definition, in ZFcard]
order_type_ext [instance, in ZFcard]
order_type_assign_rel_inv' [lemma, in ZFcard]
OrdinalUpperBound [section, in ZFord]
OrdinalUpperBound.f [variable, in ZFord]
OrdinalUpperBound.f_ord [variable, in ZFord]
OrdinalUpperBound.f_ext [variable, in ZFord]
OrdinalUpperBound.I [variable, in ZFord]
OrdinalUpperBound.supf_dir [variable, in ZFord]
ords [projection, in ModelCIC]
ords [projection, in SN_CIC]
Ordt [definition, in SN_CIC]
ord_sup_typ [lemma, in ZFord]
ord_sup [definition, in ZFord]
ord_lt_le [lemma, in ZFord]
osucc [definition, in ZFord]
OSucc [definition, in ModelCIC]
OSucc [definition, in SN_CIC]
OSucct [definition, in SN_CIC]
OSucc_sub [lemma, in SN_CIC]
OSucc_fx_sub [lemma, in SN_CIC]
osucc_morph [instance, in ZFord]
osucc_omega [lemma, in ZFord]
osucc_mono [lemma, in ZFord]
osup [definition, in ZFord]
osupf [definition, in ZFord]
osupfn [definition, in ZFord]
osupfn_mono [lemma, in ZFord]
osupf_def [lemma, in ZFord]
osupf_mono [lemma, in ZFord]
osup_lub [lemma, in ZFord]
osup_univ [lemma, in ZFord]
osup_intro [lemma, in ZFord]
osup_morph [lemma, in ZFord]
osup2 [definition, in ZFord]
osup2_relm [instance, in ZFord]
osup2_incl2 [lemma, in ZFord]
osup2_sym [lemma, in ZFord]
osup2_rel_unique [lemma, in ZFord]
osup2_ax [lemma, in ZFord]
osup2_rel [definition, in ZFord]
osup2_lub [lemma, in ZFord]
osup2_def [lemma, in ZFord]
osup2_incl1 [lemma, in ZFord]
osup2_mono [lemma, in ZFord]
osup2_rel_intro [lemma, in ZFord]
osup2_proof [lemma, in ZFord]
osup2_refl [lemma, in ZFord]
osup2_assoc [lemma, in ZFord]
osup2_morph [instance, in ZFord]
osup2_lt [lemma, in ZFord]
osup2_rel_elim [lemma, in ZFord]
OT [definition, in ZFcard]
OT [module, in SN_CIC]
OT [module, in ModelCIC]
OTeq [module, in SN_CIC]
OTeq [module, in ModelCIC]
OTeq.eq [definition, in ModelCIC]
OTeq.eq [definition, in SN_CIC]
OTeq.eq_equiv [definition, in ModelCIC]
OTeq.eq_equiv [definition, in SN_CIC]
OTeq.t [definition, in SN_CIC]
OTeq.t [definition, in ModelCIC]
OT_inj [axiom, in ZFcard]
ot_ext [lemma, in ZFcard]

P

pair [definition, in HF]
pair_inv [lemma, in ZF]
pair_equiv [lemma, in EnsUniv]
pair_intro2 [lemma, in ZF]
pair_ext [lemma, in ZF]
pair_morph [instance, in ZF]
pair_commut [lemma, in ZF]
pair_intro1 [lemma, in HF]
pair_elim [lemma, in HF]
pair_intro1 [lemma, in ZF]
pair_intro2 [lemma, in HF]
pair_elim [lemma, in ZF]
pair_morph [instance, in HF]
par_red_red [lemma, in TermECC]
par_beta [constructor, in TermECC]
par_red_red [lemma, in Term]
par_red1_subst [lemma, in TermECC]
par_red [definition, in TermECC]
par_red1 [inductive, in Term]
par_red1_subst [lemma, in Term]
par_red1_lift [lemma, in TermECC]
par_red [definition, in Term]
par_red1 [inductive, in TermECC]
par_beta [constructor, in Term]
par_beta [constructor, in TypeJudge]
par_red1_lift [lemma, in Term]
PeirceSublogicThms [module, in Sublogic]
PeirceSublogicThms.A [abbreviation, in Sublogic]
PeirceSublogicThms.Pconsistency [lemma, in Sublogic]
PeirceSublogicThms.Psl [module, in Sublogic]
PeirceTrans [module, in Sublogic]
PeirceTrans.T [definition, in Sublogic]
PeirceTrans.Tr [definition, in Sublogic]
PeirceTrans.TrCons [definition, in Sublogic]
PeirceTrans.TrI [definition, in Sublogic]
PeirceTrans.TrMono [definition, in Sublogic]
PeirceTrans.TrP [definition, in Sublogic]
permute_lift [lemma, in Lambda]
permute_lift [lemma, in Term]
permute_lift [lemma, in TermECC]
permute_lift_rec [lemma, in TermECC]
permute_lift_rec [lemma, in Lambda]
permute_lift_rec [lemma, in Term]
Pi [definition, in Can]
PI [definition, in ModelZF]
piFAM [definition, in SATnat]
piFAM_ax [lemma, in SATnat]
piNAT [definition, in SATnat]
piNATi [definition, in SATnat]
piNATi_ax [lemma, in SATnat]
piNAT_ax [lemma, in SATnat]
piSAT0 [definition, in Sat]
piSAT0_intro [lemma, in Sat]
piSAT0_elim [lemma, in Sat]
plumps [definition, in ZFord]
plumps_m [variable, in ZFord]
plumps_morph [instance, in ZFord]
plump_bound [lemma, in ZFord]
plump_set [variable, in ZFord]
plump_eqn [lemma, in ZFord]
plus_w [definition, in ZFord]
positive [record, in ZFspos]
post_fix2 [lemma, in ZFfix]
post_fix_A [lemma, in ZFfix]
post_fix1 [lemma, in ZFfix]
post_fix [definition, in ZFfix]
post_fix_lfp [lemma, in ZFfix]
pos_univ_sum [lemma, in ZFspos]
pos_mono [projection, in ZFspos]
pos_consrec [definition, in ZFspos]
pos_univ_cst [lemma, in ZFspos]
pos_sum [definition, in ZFspos]
pos_univ_rec [lemma, in ZFspos]
pos_univ_prodcart [lemma, in ZFspos]
pos_oper [projection, in ZFspos]
pos_universe [record, in ZFspos]
pos_norec [definition, in ZFspos]
pos_cst [definition, in ZFspos]
pos_param [definition, in ZFspos]
pos_oper_morph [instance, in ZFspos]
pos_univ_param [lemma, in ZFspos]
pos_rec [definition, in ZFspos]
pos_univ_norec [lemma, in ZFspos]
pos_oper_stable [lemma, in ZFspos]
power [definition, in HF]
power_mono [lemma, in ZF]
power_intro [lemma, in ZF]
power_stable [lemma, in ZFstable]
power_intro [lemma, in HF]
power_ext [lemma, in HF]
power_equiv [lemma, in EnsUniv]
power_morph [lemma, in HF]
power_morph [instance, in ZF]
power_ext [lemma, in ZF]
power_elim [lemma, in ZF]
power_elim [lemma, in HF]
prd_sup_lub [lemma, in ZFfunext]
prd_union [lemma, in ZFfunext]
prd_sup [lemma, in ZFfunext]
pred [definition, in ZFnats]
pred_succ_eq [lemma, in ZFnats]
pred_typ [lemma, in ZFnats]
pred_morph [instance, in ZFnats]
pre_fix [definition, in ZFfix]
prf_trm [definition, in HFcoc]
prf_trm [definition, in ZFcoc]
prod [abbreviation, in ZFind_nat]
Prod [constructor, in Term]
Prod [constructor, in TermECC]
prodcart [definition, in ZFpairs]
prodcart_cc_prod_iso [definition, in ZFiso]
prodcart_mono [instance, in ZFpairs]
prodcart_iso_fun_morph [lemma, in ZFiso]
prodcart_sigma_iso [definition, in ZFiso]
prodcart_stable [lemma, in ZFstable]
prodcart_comm_iso_fun [lemma, in ZFiso]
prodcart_cc_prod_iso_typ [lemma, in ZFiso]
prodcart_morph [instance, in ZFpairs]
prodcart_cc_prod_iso_morph [instance, in ZFiso]
prodcart_sigma_iso_typ [lemma, in ZFiso]
ProductContinuity [section, in ZFcont]
ProductContinuity.mu [variable, in ZFcont]
ProductContinuity.mu_ord [variable, in ZFcont]
ProductContinuity.mu_bound [variable, in ZFcont]
ProductContinuity.X [variable, in ZFcont]
ProductContinuity.X_small [variable, in ZFcont]
prod_red_l [constructor, in TermECC]
prod_red_r [constructor, in TermECC]
prod_par_red [constructor, in TermECC]
prod_red_r [constructor, in Term]
prod_red_l [constructor, in Term]
prod_par_red [constructor, in Term]
prod_par_red [constructor, in TypeJudge]
prod_eq [definition, in basic]
prop [constructor, in Term]
prop [constructor, in TermECC]
props [definition, in ZFcoc]
props [definition, in HFcoc]
props_proof_irrelevance [lemma, in ZFcoc]
push_var [definition, in SN_CIC]
push_ord [definition, in SN_CIC]
push_fun [definition, in ModelCIC]
push_var [definition, in ModelCIC]
push_fun [definition, in SN_CIC]
push_ord [definition, in ModelCIC]
P2p [definition, in ZFcoc]
p2P [definition, in ZFcoc]
p2P_morph [instance, in ZFcoc]
P2p_typ [lemma, in ZFcoc]
P2p_morph [instance, in ZFcoc]
P2p_forall [lemma, in ZFcoc]
p2P2p [lemma, in ZFcoc]
P2p2P [lemma, in ZFcoc]

Q

Q [abbreviation, in ZFord]
Qm [abbreviation, in ZFord]

R

S

T

U

V

W

X

X [axiom, in Nest]

Z

ZE [definition, in SATnat]
Zermelo_Ex_sig [module, in ZFdef]
Zermelo_Ex_sig.infinity_ex [axiom, in ZFdef]
Zermelo_sig.infinity_ax2 [axiom, in ZFdef]
Zermelo_sig.subset_ax [axiom, in ZFdef]
Zermelo_Ex_sig.subset_ex [axiom, in ZFdef]
Zermelo_sig [module, in ZFdef]
Zermelo_Ex_sig.union_ex [axiom, in ZFdef]
Zermelo_sig.infinite [axiom, in ZFdef]
Zermelo_Ex_sig.pair_ex [axiom, in ZFdef]
Zermelo_sig.subset [axiom, in ZFdef]
Zermelo_sig.power_ax [axiom, in ZFdef]
Zermelo_sig.empty_ax [axiom, in ZFdef]
Zermelo_sig.power [axiom, in ZFdef]
Zermelo_Ex_sig.empty_ex [axiom, in ZFdef]
Zermelo_sig.union [axiom, in ZFdef]
Zermelo_sig.empty [axiom, in ZFdef]
Zermelo_sig.pair [axiom, in ZFdef]
Zermelo_sig.infinity_ax1 [axiom, in ZFdef]
Zermelo_sig.union_ax [axiom, in ZFdef]
Zermelo_sig.pair_ax [axiom, in ZFdef]
Zermelo_Ex_sig.power_ex [axiom, in ZFdef]
zero [definition, in ZFnats]
ZERO [definition, in ZFind_nat]
Zero [definition, in SN_CIC]
Zero [definition, in SN_NAT]
Zero [definition, in ModelCIC]
Zero [definition, in ModelNat]
ZEROi_typ [lemma, in ZFind_nat]
ZERO_typ [lemma, in ZFind_nat]
zero_typ [lemma, in ZFnats]
zero_omega [lemma, in ZFord]
ZERO_typ_gen [lemma, in ZFind_nat]
ZF [module, in ZFskolEm]
ZF [library]
ZFcard [library]
ZFcoc [library]
ZFcont [library]
ZFdef [library]
ZFecc [library]
ZFfix [library]
ZFfixfun [library]
ZFfixrec [library]
ZFfunext [library]
ZFgrothendieck [library]
ZFind_w [library]
ZFind_wd [library]
ZFind_nat [library]
ZFind_basic [library]
ZFind_wnup [library]
ZFiso [library]
ZFlambda [library]
ZFlimit [library]
ZFlist [library]
ZFnats [library]
ZFnest [library]
ZFord [library]
ZFpack [variable, in ZFskolEm]
ZFpairs [library]
ZFrank [library]
ZFrelations [library]
ZFrepl [library]
ZFskol [library]
ZFskolEm [library]
ZFspos [library]
ZFsposd [library]
ZFstable [library]
ZFsum [library]
ZFwf [library]
ZF_sig.coll_ax [axiom, in ZFdef]
ZF_sig.coll [axiom, in ZFdef]
ZF_sig [module, in ZFdef]
ZF.coll [definition, in ZFskolEm]
ZF.coll_ax [lemma, in ZFskolEm]
ZF.EM [lemma, in ZFskolEm]

other

_ ∈ _ [notation, in EnsUniv]
_ ::: _ [notation, in HF]
_ ⊔ _ [notation, in ZFord]
_ ∩ _ [notation, in ZF]
_ ∪ _ [notation, in ZF]
_ +++ _ [notation, in HF]
_ <= _ [notation, in ZFnats]
_ ∈ _ [notation, in HF]
_ < _ [notation, in ZFnats]
_ == _ [notation, in EnsUniv]
_ == _ [notation, in HF]
_ ⊆ _ [notation, in ZF]
int0 _ _ [notation, in SN_CIC]
[ _ , _ ] \real _ [notation, in SN_NAT]
{ _ } [notation, in HF]