Pigeonhole

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

Statistics

Metric	Count
Definitions	0
Theorems exists_infinite_fiber, infinite_pigeonhole, infinite_pigeonhole_card, infinite_pigeonhole_card_lt, infinite_pigeonhole_set, le_range_of_union_finset_eq_top	6
Total	6

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	—	infinite_pigeonhole_card_lt LE.le.trans LT.lt.le
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	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	Set.Elem Set.preimage Set Set.instSingletonSet	—	instNoMaxOrder infinite_pigeonhole_card Order.succ_le_of_lt LE.le.trans LT.lt.le Order.lt_succ LT.lt.trans_le LE.le.ge isRegular_succ
infinite_pigeonhole_set 📖	mathematical	Cardinal instLE Set.Elem aleph0 Preorder.toLT PartialOrder.toPreorder partialOrder Ordinal.cof ord	Set 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 Top.top Set BooleanAlgebra.toTop Set.instBooleanAlgebra	Cardinal instLE Set.Elem Set.range	—	Set.infinite_coe_iff Set.union_finset_finite_of_range_finite Set.infinite_univ Eq.ge Set.mem_univ exists_infinite_fiber Infinite.false Finite.of_fintype Infinite.of_injective Set.inclusion_injective

---

← Back to Index