HasCardinalLT

📁 Source: Mathlib/SetTheory/Cardinal/HasCardinalLT.lean

Statistics

Metric	Count
Definitions HasCardinalLT	1
Theorems exists_regular_cardinal, exists_regular_cardinal_forall, of_injective, of_le, of_surjective, small, hasCardinalLT_aleph0_iff, hasCardinalLT_iUnion, hasCardinalLT_iff_cardinal_mk_lt, hasCardinalLT_iff_of_equiv, hasCardinalLT_lift_iff, hasCardinalLT_of_finite, hasCardinalLT_option_iff, hasCardinalLT_prod, hasCardinalLT_prod', hasCardinalLT_sigma, hasCardinalLT_sigma', hasCardinalLT_subtype_iSup, hasCardinalLT_subtype_max, hasCardinalLT_sum_iff, hasCardinalLT_ulift_iff, hasCardinalLT_union	22
Total	23

HasCardinalLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_regular_cardinal 📖	mathematical	—	Cardinal.IsRegular HasCardinalLT	—	Cardinal.isRegular_succ le_max_right hasCardinalLT_iff_of_equiv Cardinal.instNoMaxOrder
exists_regular_cardinal_forall 📖	mathematical	Small	Cardinal.IsRegular HasCardinalLT	—	exists_regular_cardinal small_sigma of_injective sigma_mk_injective
of_injective 📖	—	HasCardinalLT	—	—	Cardinal.lift_lt Cardinal.lift_lift lt_of_le_of_lt Cardinal.mk_le_of_injective ULift.up_injective ULift.down_injective
of_le 📖	—	HasCardinalLT Cardinal Cardinal.instLE	—	—	lt_of_lt_of_le
of_surjective 📖	—	HasCardinalLT	—	—	Cardinal.lift_lt Cardinal.lift_lift lt_of_le_of_lt Cardinal.mk_le_of_surjective ULift.up_surjective ULift.down_surjective
small 📖	mathematical	HasCardinalLT	Small	—	LT.lt.trans Cardinal.lift_lift Cardinal.lift_lt Cardinal.lift_lt_univ'

(root)

Definitions

Name	Category	Theorems
HasCardinalLT 📖	MathDef	24 math math: HasCardinalLT.Set.functor_obj, hasCardinalLT_of_finite, CategoryTheory.hasCardinalLT_arrow_discrete_iff, HasCardinalLT.Set.cocone_pt, CategoryTheory.hasCardinalLT_arrow_shrinkHoms_iff, hasCardinalLT_option_iff, hasCardinalLT_iff_of_equiv, CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily, HasCardinalLT.exists_regular_cardinal, CategoryTheory.Types.isCardinalPresentable_iff, hasCardinalLT_aleph0_iff, HasCardinalLT.exists_regular_cardinal_forall, CategoryTheory.SmallCategoryCardinalLT.hasCardinalLT, hasCardinalLT_ulift_iff, hasCardinalLT_sum_iff, HasCardinalLT.Set.cocone_ι_app, HasCardinalLT.Set.functor_map_coe, CategoryTheory.hasCardinalLT_arrow_op_iff, HasCardinalLT.Set.instIsCardinalFiltered, hasCardinalLT_iff_cardinal_mk_lt, HasCardinalLT.Set.instIsFilteredOfFactIsRegular, CategoryTheory.hasCardinalLT_arrow_shrink_iff, HasCardinalLT.Set.isFiltered_of_aleph0_le, hasCardinalLT_lift_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCardinalLT_aleph0_iff 📖	mathematical	—	HasCardinalLT Cardinal.aleph0 Finite	—	Cardinal.lift_aleph0 Cardinal.mk_lt_aleph0_iff
hasCardinalLT_iUnion 📖	mathematical	HasCardinalLT Set.Elem	Set.iUnion	—	Set.ext iSup_apply iSup_Prop_eq hasCardinalLT_subtype_iSup
hasCardinalLT_iff_cardinal_mk_lt 📖	mathematical	—	HasCardinalLT Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder	—	Cardinal.lift_id
hasCardinalLT_iff_of_equiv 📖	mathematical	—	HasCardinalLT	—	HasCardinalLT.of_injective Equiv.injective
hasCardinalLT_lift_iff 📖	mathematical	—	HasCardinalLT Cardinal.lift	—	Cardinal.lift_lift StrictMono.lt_iff_lt Cardinal.lift_strictMono
hasCardinalLT_of_finite 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0	HasCardinalLT	—	HasCardinalLT.of_le hasCardinalLT_aleph0_iff
hasCardinalLT_option_iff 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0	HasCardinalLT	—	hasCardinalLT_iff_of_equiv hasCardinalLT_sum_iff HasCardinalLT.of_le hasCardinalLT_aleph0_iff Finite.of_fintype
hasCardinalLT_prod 📖	—	Cardinal Cardinal.instLE Cardinal.aleph0 HasCardinalLT	—	—	hasCardinalLT_prod' HasCardinalLT.of_surjective
hasCardinalLT_prod' 📖	—	Cardinal Cardinal.instLE Cardinal.aleph0 HasCardinalLT	—	—	hasCardinalLT_iff_cardinal_mk_lt Cardinal.mk_prod Cardinal.lift_id Cardinal.mul_lt_of_lt
hasCardinalLT_sigma 📖	—	HasCardinalLT	—	—	Cardinal.IsRegular.lift Fact.out hasCardinalLT_sigma' HasCardinalLT.of_surjective hasCardinalLT_lift_iff
hasCardinalLT_sigma' 📖	—	HasCardinalLT	—	—	Cardinal.mk_sigma Cardinal.sum_lt_lift_of_isRegular Fact.out Cardinal.lift_id
hasCardinalLT_subtype_iSup 📖	mathematical	HasCardinalLT	iSup Pi.supSet ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Prop.instCompleteLinearOrder	—	HasCardinalLT.of_surjective hasCardinalLT_sigma iSup_apply iSup_Prop_eq
hasCardinalLT_subtype_max 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 HasCardinalLT	Pi.instMaxForall_mathlib SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Prop.instCompleteLinearOrder	—	hasCardinalLT_sum_iff HasCardinalLT.of_surjective
hasCardinalLT_sum_iff 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0	HasCardinalLT	—	HasCardinalLT.of_injective Sum.inl_injective Sum.inr_injective Cardinal.mk_sum Cardinal.lift_add Cardinal.lift_lift Cardinal.add_lt_of_lt Cardinal.lift_lt
hasCardinalLT_ulift_iff 📖	mathematical	—	HasCardinalLT	—	hasCardinalLT_iff_of_equiv
hasCardinalLT_union 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 HasCardinalLT Set.Elem	Set Set.instUnion	—	hasCardinalLT_subtype_max

---

← Back to Index