AhlswedeZhang

📁 Source: Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean

Statistics

Metric	Count
Definitions `infSum`, `supSum`, `truncatedInf`, `truncatedSup`	4
Theorems `le_infSum`, `infSum_compls_add_supSum`, `infSum_eq_one`, `infSum_union_add_infSum_sups`, `supSum_of_univ_notMem`, `supSum_singleton`, `supSum_union_add_supSum_infs`, `card_truncatedInf_union_add_card_truncatedInf_sups`, `card_truncatedSup_union_add_card_truncatedSup_infs`, `compl_truncatedInf`, `compl_truncatedSup`, `le_truncatedSup`, `map_truncatedInf`, `map_truncatedSup`, `truncatedInf_empty`, `truncatedInf_le`, `truncatedInf_of_isAntichain`, `truncatedInf_of_mem`, `truncatedInf_of_notMem`, `truncatedInf_singleton`, `truncatedInf_sups`, `truncatedInf_sups_of_notMem`, `truncatedInf_union`, `truncatedInf_union_left`, `truncatedInf_union_of_notMem`, `truncatedInf_union_right`, `truncatedSup_empty`, `truncatedSup_infs`, `truncatedSup_infs_of_notMem`, `truncatedSup_of_isAntichain`, `truncatedSup_of_mem`, `truncatedSup_of_notMem`, `truncatedSup_singleton`, `truncatedSup_union`, `truncatedSup_union_left`, `truncatedSup_union_of_notMem`, `truncatedSup_union_right`	37
Total	41

AhlswedeZhang

Definitions

Name	Category	Theorems
`infSum` 📖	CompOp	4 math math: `infSum_eq_one`, `IsAntichain.le_infSum`, `infSum_compls_add_supSum`, `infSum_union_add_infSum_sups`
`supSum` 📖	CompOp	4 math math: `supSum_union_add_supSum_infs`, `infSum_compls_add_supSum`, `supSum_of_univ_notMem`, `supSum_singleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infSum_compls_add_supSum` 📖	mathematical	—	`infSum` `Finset.compls` `Finset` `Finset.booleanAlgebra` `supSum` `Fintype.card` `Finset.sum` `Rat.addCommMonoid` `Finset.range`	—	`compl_injective` `Finset.map_univ_of_surjective` `compl_surjective` `Finset.sum_map` `Finset.sum_congr` `Finset.card_compl` `Nat.cast_sub` `Finset.card_le_univ` `Nat.choose_symm` `Finset.univ_map_embedding` `sub_add_cancel`
`infSum_eq_one` 📖	mathematical	`Finset.Nonempty` `Finset` `Finset.instMembership` `Finset.instEmptyCollection`	`infSum`	—	`Finset.compls_compls` `eq_sub_of_add_eq` `infSum_compls_add_supSum` `supSum_of_univ_notMem` `Finset.Nonempty.compls` `Finset.compl_univ` `add_sub_cancel_left`
`infSum_union_add_infSum_sups` 📖	mathematical	—	`infSum` `Finset` `Finset.instUnion` `Finset.decidableEq` `HasSups.sups` `Finset.hasSups` `Lattice.toSemilatticeSup` `Finset.instLattice`	—	`Finset.sum_add_distrib` `Finset.sum_congr` `Finset.card_truncatedInf_union_add_card_truncatedInf_sups`
`supSum_of_univ_notMem` 📖	mathematical	`Finset.Nonempty` `Finset` `Finset.instMembership` `Finset.univ`	`supSum` `Fintype.card` `Finset.sum` `Rat.addCommMonoid` `Finset.range`	—	`Finset.Nonempty.exists_eq_singleton_or_nontrivial` `supSum_singleton` `LT.lt.ne` `Finset.Nonempty.card_pos` `Finset.card_eq_succ` `Finset.instLawfulSingleton` `Finset.insert_eq` `eq_sub_of_add_eq` `supSum_union_add_supSum_infs` `Finset.singleton_infs` `Finset.mem_insert_self` `lt_add_one` `Nat.instZeroLEOneClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.mem_insert_of_mem` `LE.le.trans_lt` `Finset.card_image_le` `Finset.Nonempty.image` `add_sub_cancel_right`
`supSum_singleton` 📖	mathematical	—	`supSum` `Finset` `Finset.instSingleton` `Fintype.card` `Finset.sum` `Rat.addCommMonoid` `Finset.range`	—	`Finset.truncatedSup_singleton` `sub_self` `zero_div` `sub_eq_of_eq_add` `Finset.sum_congr` `Finset.sum_ite` `Finset.sum_const_zero` `add_zero` `Finset.filter_subset_univ` `Finset.sum_powerset` `Finset.card_lt_iff_ne_univ` `mul_div_assoc` `nsmul_eq_mul` `Finset.sum_powersetCard`
`supSum_union_add_supSum_infs` 📖	mathematical	—	`supSum` `Finset` `Finset.instUnion` `Finset.decidableEq` `HasInfs.infs` `Finset.hasInfs` `Lattice.toSemilatticeInf` `Finset.instLattice`	—	`Finset.sum_add_distrib` `Finset.sum_congr` `Finset.card_truncatedSup_union_add_card_truncatedSup_infs`

AhlswedeZhang.IsAntichain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_infSum` 📖	mathematical	`IsAntichain` `Finset` `Finset.instHasSubset` `SetLike.coe` `Finset.instSetLike` `Finset.instMembership` `Finset.instEmptyCollection`	`Finset.sum` `Rat.addCommMonoid` `Nat.choose` `Fintype.card` `Finset.card` `AhlswedeZhang.infSum`	—	`Finset.sum_congr` `Finset.truncatedInf_of_isAntichain` `div_mul_cancel_left₀` `Finset.Nonempty.card_pos` `Finset.nonempty_iff_ne_empty` `ne_of_gt` `Nat.cast_pos'` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `NeZero.one` `Rat.nontrivial` `Finset.sum_le_univ_sum_of_nonneg` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Rat.instIsStrictOrderedRing` `Nat.cast_nonneg'` `mul_nonneg` `Rat.instPosMulMono`

Finset

Definitions

Name	Category	Theorems
`truncatedInf` 📖	CompOp	16 math math: `map_truncatedInf`, `truncatedInf_of_isAntichain`, `truncatedInf_union`, `truncatedInf_le`, `truncatedInf_union_of_notMem`, `truncatedInf_union_left`, `truncatedInf_empty`, `card_truncatedInf_union_add_card_truncatedInf_sups`, `truncatedInf_singleton`, `truncatedInf_sups_of_notMem`, `truncatedInf_sups`, `compl_truncatedInf`, `compl_truncatedSup`, `truncatedInf_union_right`, `truncatedInf_of_mem`, `truncatedInf_of_notMem`
`truncatedSup` 📖	CompOp	16 math math: `truncatedSup_infs`, `truncatedSup_union_of_notMem`, `le_truncatedSup`, `truncatedSup_of_mem`, `truncatedSup_empty`, `truncatedSup_singleton`, `truncatedSup_union`, `truncatedSup_union_left`, `truncatedSup_union_right`, `map_truncatedSup`, `compl_truncatedInf`, `truncatedSup_infs_of_notMem`, `truncatedSup_of_isAntichain`, `truncatedSup_of_notMem`, `compl_truncatedSup`, `card_truncatedSup_union_add_card_truncatedSup_infs`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_truncatedInf_union_add_card_truncatedInf_sups` 📖	mathematical	—	`card` `truncatedInf` `Finset` `Lattice.toSemilatticeInf` `instLattice` `instDecidableLE` `boundedOrder` `instUnion` `decidableEq` `HasSups.sups` `hasSups` `Lattice.toSemilatticeSup`	—	`truncatedInf_union` `truncatedInf_sups` `card_inter_add_card_union` `truncatedInf_union_left` `truncatedInf_of_notMem` `truncatedInf_sups_of_notMem` `truncatedInf_union_right` `add_comm` `truncatedInf_union_of_notMem`
`card_truncatedSup_union_add_card_truncatedSup_infs` 📖	mathematical	—	`card` `truncatedSup` `Finset` `Lattice.toSemilatticeSup` `instLattice` `instDecidableLE` `CoheytingAlgebra.toOrderTop` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `booleanAlgebra` `instUnion` `decidableEq` `HasInfs.infs` `hasInfs` `Lattice.toSemilatticeInf`	—	`truncatedSup_union` `truncatedSup_infs` `card_union_add_card_inter` `truncatedSup_union_left` `truncatedSup_of_notMem` `truncatedSup_infs_of_notMem` `truncatedSup_union_right` `add_comm` `truncatedSup_union_of_notMem`
`compl_truncatedInf` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl` `truncatedInf` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `truncatedSup` `Lattice.toSemilatticeSup` `CoheytingAlgebra.toOrderTop` `compls`	—	`map_truncatedInf`
`compl_truncatedSup` 📖	mathematical	—	`Compl.compl` `BooleanAlgebra.toCompl` `truncatedSup` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `CoheytingAlgebra.toOrderTop` `truncatedInf` `Lattice.toSemilatticeInf` `BooleanAlgebra.toBoundedOrder` `compls`	—	`map_truncatedSup`
`le_truncatedSup` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `truncatedSup`	—	`truncatedSup.eq_1` `LE.le.trans` `le_sup'` `mem_filter` `le_top`
`map_truncatedInf` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `instFunLikeOrderIso` `truncatedInf` `map` `Equiv.toEmbedding` `RelIso.toEquiv`	—	`coe_map` `Set.image_congr` `upperClosure_image` `OrderIso.symm_apply_apply` `map_finset_inf'` `InfTopHomClass.toInfHomClass` `OrderIsoClass.toInfTopHomClass` `OrderIso.instOrderIsoClass` `BotHomClass.map_bot` `OrderIsoClass.toBotHomClass` `map_nonempty` `filter_map` `filter.congr_simp` `inf'_congr` `inf'_map`
`map_truncatedSup` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLikeOrderIso` `truncatedSup` `BoundedOrder.toOrderTop` `map` `Equiv.toEmbedding` `RelIso.toEquiv`	—	`coe_map` `Set.image_congr` `lowerClosure_image` `OrderIso.symm_apply_apply` `map_finset_sup'` `OrderIsoClass.toSupHomClass` `OrderIso.instOrderIsoClass` `TopHomClass.map_top` `OrderIsoClass.toTopHomClass` `map_nonempty` `filter_map` `filter.congr_simp` `sup'_congr` `sup'_map`
`truncatedInf_empty` 📖	mathematical	—	`truncatedInf` `Finset` `instEmptyCollection` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `BoundedOrder.toOrderBot`	—	`truncatedInf_of_notMem` `coe_empty` `upperClosure_empty`
`truncatedInf_le` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `truncatedInf`	—	`LE.le.trans'` `inf'_le` `mem_filter` `bot_le`
`truncatedInf_of_isAntichain` 📖	mathematical	`IsAntichain` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.coe` `Finset` `instSetLike` `instMembership`	`truncatedInf`	—	`le_antisymm` `truncatedInf_le` `subset_upperClosure` `truncatedInf_of_mem` `Eq.ge` `IsAntichain.eq`
`truncatedInf_of_mem` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.instMembership` `UpperSet.instSetLike` `upperClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedInf` `inf'` `filter`	—	—
`truncatedInf_of_notMem` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.instMembership` `UpperSet.instSetLike` `upperClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedInf` `Bot.bot` `OrderBot.toBot` `BoundedOrder.toOrderBot`	—	—
`truncatedInf_singleton` 📖	mathematical	—	`truncatedInf` `Finset` `instSingleton` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Bot.bot` `OrderBot.toBot` `BoundedOrder.toOrderBot`	—	`coe_singleton` `upperClosure_singleton` `inf'_congr` `filter_true_of_mem`
`truncatedInf_sups` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `SetLike.instMembership` `UpperSet.instSetLike` `upperClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedInf` `HasSups.sups` `hasSups` `Lattice.toSemilatticeSup` `SemilatticeSup.toMax`	—	`filter_sups_le` `Nonempty.product` `truncatedInf_of_mem` `inf'_congr` `inf'_sup_inf'` `Nonempty.of_image` `inf'_image`
`truncatedInf_sups_of_notMem` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `SetLike.instMembership` `UpperSet.instSetLike` `UpperSet.instMax` `upperClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedInf` `HasSups.sups` `hasSups` `Lattice.toSemilatticeSup` `Bot.bot` `OrderBot.toBot` `BoundedOrder.toOrderBot`	—	`truncatedInf_of_notMem` `coe_sups` `upperClosure_sups`
`truncatedInf_union` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.instMembership` `UpperSet.instSetLike` `upperClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedInf` `instUnion` `SemilatticeInf.toMin`	—	`filter_union` `truncatedInf_of_mem` `inf'_congr` `inf'_union`
`truncatedInf_union_left` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.instMembership` `UpperSet.instSetLike` `upperClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedInf` `instUnion`	—	`filter_union` `filter_false_of_mem` `union_empty` `truncatedInf_of_mem` `inf'_congr`
`truncatedInf_union_of_notMem` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.instMembership` `UpperSet.instSetLike` `upperClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedInf` `instUnion` `Bot.bot` `OrderBot.toBot` `BoundedOrder.toOrderBot`	—	`truncatedInf_of_notMem` `coe_union` `upperClosure_union`
`truncatedInf_union_right` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.instMembership` `UpperSet.instSetLike` `upperClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedInf` `instUnion`	—	`union_comm` `truncatedInf_union_left`
`truncatedSup_empty` 📖	mathematical	—	`truncatedSup` `Finset` `instEmptyCollection` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`truncatedSup_of_notMem` `coe_empty` `lowerClosure_empty`
`truncatedSup_infs` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `SetLike.instMembership` `LowerSet.instSetLike` `lowerClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedSup` `Lattice.toSemilatticeSup` `BoundedOrder.toOrderTop` `SemilatticeSup.toPartialOrder` `HasInfs.infs` `hasInfs` `SemilatticeInf.toMin`	—	`filter_infs_le` `Nonempty.product` `truncatedSup_of_mem` `sup'_congr` `sup'_inf_sup'` `Nonempty.of_image` `sup'_image`
`truncatedSup_infs_of_notMem` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `SetLike.instMembership` `LowerSet.instSetLike` `LowerSet.instMin` `lowerClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedSup` `Lattice.toSemilatticeSup` `BoundedOrder.toOrderTop` `SemilatticeSup.toPartialOrder` `HasInfs.infs` `hasInfs` `Top.top` `OrderTop.toTop`	—	`truncatedSup_of_notMem` `coe_infs` `lowerClosure_infs`
`truncatedSup_of_isAntichain` 📖	mathematical	`IsAntichain` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.coe` `Finset` `instSetLike` `instMembership`	`truncatedSup`	—	`le_antisymm` `subset_lowerClosure` `truncatedSup_of_mem` `Eq.ge` `IsAntichain.eq` `le_truncatedSup`
`truncatedSup_of_mem` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `LowerSet.instSetLike` `lowerClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedSup` `sup'` `filter`	—	—
`truncatedSup_of_notMem` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `LowerSet.instSetLike` `lowerClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedSup` `Top.top` `OrderTop.toTop`	—	—
`truncatedSup_singleton` 📖	mathematical	—	`truncatedSup` `Finset` `instSingleton` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Top.top` `OrderTop.toTop`	—	`coe_singleton` `lowerClosure_singleton` `sup'_congr` `filter_true_of_mem`
`truncatedSup_union` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `LowerSet.instSetLike` `lowerClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedSup` `instUnion` `SemilatticeSup.toMax`	—	`filter_union` `truncatedSup_of_mem` `sup'_congr` `sup'_union`
`truncatedSup_union_left` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `LowerSet.instSetLike` `lowerClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedSup` `instUnion`	—	`filter_union` `filter_false_of_mem` `union_empty` `truncatedSup_of_mem` `sup'_congr`
`truncatedSup_union_of_notMem` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `LowerSet.instSetLike` `lowerClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedSup` `instUnion` `Top.top` `OrderTop.toTop`	—	`truncatedSup_of_notMem`
`truncatedSup_union_right` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.instMembership` `LowerSet.instSetLike` `lowerClosure` `SetLike.coe` `Finset` `instSetLike`	`truncatedSup` `instUnion`	—	`union_comm` `truncatedSup_union_left`

---

← Back to Index