Pigeonhole

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

Statistics

Metric	Count
Definitions	0
Theorems exists_infinite_fiber, exists_infinite_fiber', exists_uncountable_fiber, infinite_pigeonhole, infinite_pigeonhole_card, infinite_pigeonhole_card_lt, infinite_pigeonhole_set, le_range_of_union_finset_eq_top, le_range_of_union_finset_eq_univ	9
Total	9

Cardinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_infinite_fiber 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder	Infinite Set.Elem Set.preimage Set Set.instSingletonSet	—	lt_or_ge infinite_pigeonhole_card le_rfl IsRegular.cof_ord isRegular_aleph0 infinite_pigeonhole_card_lt LE.le.trans LT.lt.le
exists_infinite_fiber' 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder	Infinite Set.Elem Set.preimage Set Set.instSingletonSet	—	Infinite.of_cardinalMk_le LT.lt.le exists_infinite_fiber
exists_uncountable_fiber 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder	Uncountable Set.Elem Set.preimage Set Set.instSingletonSet	—	lt_or_ge infinite_pigeonhole_card LT.lt.le aleph0_lt_aleph_one IsRegular.cof_ord isRegular_aleph_one LT.lt.trans infinite_pigeonhole_card_lt instInfiniteOfUncountable LE.le.trans succ_aleph0 Order.succ_le_succ_iff instNoMaxOrder Order.succ_le_of_lt
infinite_pigeonhole 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal.cof ord	Set.Elem Set.preimage Set Set.instSingletonSet	—	Eq.not_lt mk_univ Set.preimage_univ Set.iUnion_of_singleton Set.preimage_iUnion LE.le.trans_lt sum_le_mk_mul_iSup mul_lt_of_lt LT.lt.trans_le Ordinal.cof_ord_le Ordinal.iSup_lt LE.le.antisymm' le_mk_iff_exists_set
infinite_pigeonhole_card 📖	mathematical	Cardinal instLE aleph0 Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal.cof ord	Cardinal instLE Set.Elem Set.preimage Set Set.instSingletonSet	—	le_mk_iff_exists_set infinite_pigeonhole Set.preimage_comp mk_preimage_of_injective Subtype.val_injective
infinite_pigeonhole_card_lt 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder	Cardinal Preorder.toLT PartialOrder.toPreorder partialOrder Set.Elem Set.preimage Set Set.instSingletonSet	—	instNoMaxOrder lt_or_ge infinite_pigeonhole_card le_rfl IsRegular.cof_ord isRegular_aleph0 LE.le.trans' Order.succ_le_of_lt LE.le.trans Order.le_succ LT.lt.trans_le Order.lt_succ LE.le.ge IsRegular.le_cof_ord isRegular_succ
infinite_pigeonhole_set 📖	mathematical	Cardinal instLE Set.Elem aleph0 Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal.cof ord	Set Set.instHasSubset Cardinal instLE Set.Elem Set.instMembership	—	infinite_pigeonhole_card LE.le.trans ge_of_eq
le_range_of_union_finset_eq_top 📖	mathematical	Set.iUnion SetLike.coe Finset Finset.instSetLike Set.univ	Cardinal instLE Set.Elem Finset Set.range	—	le_range_of_union_finset_eq_univ
le_range_of_union_finset_eq_univ 📖	mathematical	Set.iUnion SetLike.coe Finset Finset.instSetLike Set.univ	Cardinal instLE Set.Elem Finset Set.range	—	Eq.ge Set.mem_univ exists_infinite_fiber Infinite.false Finite.of_fintype Infinite.of_injective Set.inclusion_injective

---

← Back to Index