Card

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/Card.lean

Statistics

Metric	Count
Definitions generateMeasurableRec	1
Theorems cardinal_generateMeasurableRec_le, cardinal_generateMeasurable_le, cardinal_generateMeasurable_le_continuum, cardinal_measurableSet_le, cardinal_measurableSet_le_continuum, compl_mem_generateMeasurableRec, empty_mem_generateMeasurableRec, generateMeasurableRec_induction, generateMeasurableRec_mono, generateMeasurableRec_of_omega1_le, generateMeasurableRec_of_omega_one_le, generateMeasurableRec_omega1, generateMeasurableRec_omega_one, generateMeasurableRec_subset, generateMeasurable_eq_rec, iUnion_mem_generateMeasurableRec, self_subset_generateMeasurableRec	17
Total	18

MeasurableSpace

Definitions

Name	Category	Theorems
generateMeasurableRec 📖	CompOp	10 math math: self_subset_generateMeasurableRec, generateMeasurableRec_of_omega_one_le, cardinal_generateMeasurableRec_le, empty_mem_generateMeasurableRec, generateMeasurableRec_mono, generateMeasurableRec_omega_one, generateMeasurableRec_of_omega1_le, generateMeasurableRec_omega1, generateMeasurableRec_subset, generateMeasurable_eq_rec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinal_generateMeasurableRec_le 📖	mathematical	—	Cardinal Cardinal.instLE Set.Elem Set generateMeasurableRec Cardinal.instPowCardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat Cardinal.aleph0	—	Nat.instAtLeastTwoHAddOfNat WellFoundedLT.induction Ordinal.wellFoundedLT Cardinal.power_le_power_right le_max_right LE.le.trans Cardinal.aleph0_le_continuum Cardinal.mk_biUnion_le_of_le_lift Cardinal.lift_power Cardinal.lift_aleph0 Cardinal.card_le_of_le_ord Cardinal.ord_aleph Ordinal.lift_one Ordinal.lift_omega Ordinal.lift_le Ordinal.lift_card Cardinal.aleph_one_le_continuum Cardinal.lift_max Cardinal.lift_ofNat LT.lt.le LT.lt.trans_le generateMeasurableRec.eq_1 Cardinal.mk_union_le Cardinal.add_le_of_le Cardinal.self_le_power Cardinal.one_le_aleph0 le_max_left Cardinal.mk_singleton Cardinal.one_lt_aleph0 Cardinal.mk_image_le Cardinal.mk_range_le Cardinal.mk_pi Cardinal.prod_const Cardinal.lift_uzero Cardinal.mk_denumerable Cardinal.aleph0_mul_aleph0 Cardinal.power_mul le_or_gt generateMeasurableRec_of_omega_one_le le_rfl
cardinal_generateMeasurable_le 📖	mathematical	—	Cardinal Cardinal.instLE Set.Elem Set setOf GenerateMeasurable Cardinal.instPowCardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat Cardinal.aleph0	—	Nat.instAtLeastTwoHAddOfNat cardinal_generateMeasurableRec_le
cardinal_generateMeasurable_le_continuum 📖	mathematical	—	Cardinal Cardinal.instLE Set.Elem Set setOf GenerateMeasurable Cardinal.continuum	—	LE.le.trans Nat.instAtLeastTwoHAddOfNat cardinal_generateMeasurable_le Cardinal.continuum_power_aleph0 Cardinal.power_le_power_right max_le LT.lt.le Cardinal.nat_lt_continuum
cardinal_measurableSet_le 📖	mathematical	—	Cardinal Cardinal.instLE Set.Elem Set setOf MeasurableSet generateFrom Cardinal.instPowCardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat Cardinal.aleph0	—	cardinal_generateMeasurable_le
cardinal_measurableSet_le_continuum 📖	mathematical	—	Cardinal Cardinal.instLE Set.Elem Set setOf MeasurableSet generateFrom Cardinal.continuum	—	cardinal_generateMeasurable_le_continuum
compl_mem_generateMeasurableRec 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Set Set.instMembership generateMeasurableRec	Compl.compl Set.instCompl	—	generateMeasurableRec.eq_def Set.mem_union_left Set.mem_union_right Set.mem_iUnion₂
empty_mem_generateMeasurableRec 📖	mathematical	—	Set Set.instMembership generateMeasurableRec Set.instEmptyCollection	—	generateMeasurableRec.eq_def Set.mem_union_left Set.mem_union_right Set.mem_singleton
generateMeasurableRec_induction 📖	—	Set Set.instEmptyCollection Compl.compl Set.instCompl Set.iUnion Set.instMembership generateMeasurableRec	—	—	WellFoundedLT.induction Ordinal.wellFoundedLT LE.le.trans LT.lt.le generateMeasurableRec.eq_def LT.lt.trans_le Set.mem_iUnion₂ le_rfl
generateMeasurableRec_mono 📖	mathematical	—	Monotone Ordinal Set PartialOrder.toPreorder Ordinal.partialOrder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra generateMeasurableRec	—	LE.le.eq_or_lt Set.iUnion_const iUnion_mem_generateMeasurableRec
generateMeasurableRec_of_omega1_le 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding Ordinal.omega Ordinal.one	generateMeasurableRec	—	generateMeasurableRec_of_omega_one_le
generateMeasurableRec_of_omega_one_le 📖	mathematical	Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding Ordinal.omega Ordinal.one	generateMeasurableRec	—	LE.le.antisymm' generateMeasurableRec_mono generateMeasurableRec_subset
generateMeasurableRec_omega1 📖	mathematical	—	generateMeasurableRec DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instFunLikeOrderEmbedding Ordinal.omega Ordinal.one Set.iUnion Set Preorder.toLT	—	generateMeasurableRec_omega_one
generateMeasurableRec_omega_one 📖	mathematical	—	generateMeasurableRec DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instFunLikeOrderEmbedding Ordinal.omega Ordinal.one Set.iUnion Set Preorder.toLT	—	HasSubset.Subset.antisymm' Set.instAntisymmSubset Set.iUnion₂_subset generateMeasurableRec_mono LT.lt.le Set.mem_iUnion₂ generateMeasurableRec_induction Ordinal.omega_pos self_subset_generateMeasurableRec empty_mem_generateMeasurableRec Order.IsSuccLimit.succ_lt Cardinal.isSuccLimit_omega compl_mem_generateMeasurableRec Order.lt_succ Ordinal.instNoMaxOrder Ordinal.lsub_lt_ord_lift Cardinal.mk_nat Cardinal.lift_aleph0 Cardinal.IsRegular.cof_omega_eq Cardinal.isRegular_aleph_one Cardinal.aleph0_lt_aleph_one iUnion_mem_generateMeasurableRec Ordinal.lt_lsub
generateMeasurableRec_subset 📖	mathematical	—	Set Set.instHasSubset generateMeasurableRec setOf GenerateMeasurable	—	WellFoundedLT.induction Ordinal.wellFoundedLT generateMeasurableRec_induction
generateMeasurable_eq_rec 📖	mathematical	—	setOf Set GenerateMeasurable generateMeasurableRec DFunLike.coe OrderEmbedding Ordinal Preorder.toLE PartialOrder.toPreorder Ordinal.partialOrder instFunLikeOrderEmbedding Ordinal.omega Ordinal.one	—	HasSubset.Subset.antisymm' Set.instAntisymmSubset generateMeasurableRec_subset self_subset_generateMeasurableRec empty_mem_generateMeasurableRec Set.mem_iUnion₂ generateMeasurableRec_omega_one generateMeasurableRec_mono LT.lt.le Order.IsSuccLimit.succ_lt Cardinal.isSuccLimit_omega compl_mem_generateMeasurableRec Order.lt_succ Ordinal.instNoMaxOrder iUnion_mem_generateMeasurableRec
iUnion_mem_generateMeasurableRec 📖	mathematical	Ordinal Preorder.toLT PartialOrder.toPreorder Ordinal.partialOrder Set Set.instMembership generateMeasurableRec	Set.iUnion	—	generateMeasurableRec.eq_def Set.mem_union_right Set.mem_iUnion₂
self_subset_generateMeasurableRec 📖	mathematical	—	Set Set.instHasSubset generateMeasurableRec	—	generateMeasurableRec.eq_def Set.subset_union_of_subset_left subset_rfl Set.instReflSubset

---

← Back to Index