Documentation Verification Report

FourFunctions

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

Statistics

Metric	Count
Definitions	0
Theorems `card_le_card_diffs`, `four_functions_theorem`, `le_card_diffs_mul_card_diffs`, `le_card_infs_mul_card_sups`, `collapse_eq`, `collapse_modular`, `collapse_nonneg`, `collapse_of_mem`, `fkg`, `four_functions_theorem`, `four_functions_theorem_univ`, `holley`, `le_collapse_of_insert_mem`, `le_collapse_of_mem`, `sum_collapse`	15
Total	15

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_card_diffs` 📖	mathematical	—	`card` `diffs`	—	`le_of_pow_le_pow_left₀` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `IsOrderedRing.toMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `two_ne_zero` `zero_le` `Nat.instCanonicallyOrderedAdd` `le_card_diffs_mul_card_diffs`
`four_functions_theorem` 📖	mathematical	`Pi.hasLe` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instInter` `instUnion` `instHasSubset` `powerset`	`sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `HasInfs.infs` `hasInfs` `decidableEq` `instLattice` `HasSups.sups` `hasSups` `Lattice.toSemilatticeSup`	—	`induction` `MulZeroClass.mul_zero` `sum_congr` `infs_empty` `sups_empty` `sum_singleton` `MulZeroClass.zero_mul` `infs_singleton` `inf_of_le_right` `sups_singleton` `sup_of_le_left` `image_singleton` `subset_refl` `instReflSubset` `subset_rfl` `powerset_infs_powerset_self` `infs_subset` `powerset_sups_powerset_self` `sups_subset` `sum_collapse` `collapse_nonneg` `collapse_modular` `Subset.rfl`
`le_card_diffs_mul_card_diffs` 📖	mathematical	—	`card` `diffs`	—	`Booleanisation.liftLatticeHom_injective` `map_eq_image` `image_image₂_distrib` `card_map` `card_compls` `infs_compls_eq_diffs` `compls_sups` `compls_compls` `compls_infs_eq_diffs` `le_card_infs_mul_card_sups`
`le_card_infs_mul_card_sups` 📖	mathematical	—	`card` `HasInfs.infs` `Finset` `hasInfs` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `HasSups.sups` `hasSups` `Lattice.toSemilatticeSup`	—	`sum_congr` `sum_const` `nsmul_eq_mul` `mul_one` `four_functions_theorem` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `zero_le_one` `Pi.instZeroLEOneClass` `Nat.instZeroLEOneClass` `le_rfl`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`collapse_eq` 📖	mathematical	`Finset` `Finset.instMembership`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.decidableMem` `Finset.decidableEq` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finset.instInsert`	—	`Finset.sum_congr` `Finset.sum_insert` `Finset.mem_insert_self` `Finset.sum_singleton` `add_zero` `zero_add`
`collapse_modular` 📖	mathematical	`Finset` `Finset.instMembership` `Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Finset.instInter` `Finset.instUnion` `Finset.instHasSubset`	`HasInfs.infs` `Finset.hasInfs` `Finset.decidableEq` `Finset.instLattice` `HasSups.sups` `Finset.hasSups` `Lattice.toSemilatticeSup`	—	`HasSubset.Subset.trans` `Finset.instIsTransSubset` `Finset.subset_insert` `Finset.insert_subset_insert` `Finset.notMem_mono` `Finset.inter_subset_left` `Finset.notMem_union` `collapse_eq` `collapse_of_mem` `Finset.inter_mem_infs` `Finset.insert_inter_distrib` `Finset.union_mem_sups` `Finset.insert_union_distrib` `Finset.union_insert` `Finset.insert_union` `Finset.insert_eq_of_mem` `Finset.insert_inter_of_notMem` `Finset.inter_insert_of_notMem` `Finset.inter_insert_of_mem` `add_zero` `add_mul` `Distrib.rightDistribClass` `LE.le.trans` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `mul_add` `Distrib.leftDistribClass` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_collapse_of_mem` `add_nonneg` `zero_add` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `le_collapse_of_insert_mem` `MulZeroClass.mul_zero` `mul_nonneg` `collapse_nonneg` `mul_le_mul` `MulZeroClass.zero_mul`
`collapse_nonneg` 📖	—	`Pi.hasLe` `Finset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—	`Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`collapse_of_mem` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.instInsert`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`collapse_eq`
`fkg` 📖	mathematical	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monotone` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SemilatticeInf.toMin` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ`	—	`four_functions_theorem_univ` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Pi.isOrderedRing` `IsStrictOrderedRing.toIsOrderedRing` `mul_mul_mul_comm` `mul_assoc` `mul_le_mul` `IsOrderedRing.toMulPosMono` `le_sup_left` `le_sup_right`
`four_functions_theorem` 📖	mathematical	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SemilatticeInf.toMin` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `HasInfs.infs` `Finset` `Finset.hasInfs` `HasSups.sups` `Finset.hasSups`	—	`IsSublattice.supClosed` `isSublattice_latticeClosure` `IsSublattice.infClosed` `Set.Finite.to_subtype` `Set.Finite.latticeClosure` `Set.Finite.union` `Finset.finite_toSet` `Function.Injective.injOn` `Subtype.coe_injective` `Finset.map_eq_image` `Finset.image_preimage` `Finset.filter.congr_simp` `Subtype.range_coe_subtype` `subset_latticeClosure` `Set.subset_union_left` `Set.subset_union_right` `exists_birkhoff_representation` `Finite.of_fintype` `Function.extend_nonneg` `le_rfl` `em` `LatticeHomClass.toSupHomClass` `LatticeHom.instLatticeHomClass` `LatticeHomClass.toInfHomClass` `Function.Injective.extend_apply` `Function.extend_apply'` `MulZeroClass.mul_zero` `mul_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `MulZeroClass.zero_mul` `Finset.sum_congr` `Finset.sum_map`
`four_functions_theorem_univ` 📖	mathematical	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SemilatticeInf.toMin` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ`	—	`Finset.sum_congr` `Finset.univ_infs_univ` `Finset.univ_sups_univ` `four_functions_theorem`
`holley` 📖	—	`Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monotone` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SemilatticeInf.toMin` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—	`LE.le.eq_or_lt` `Finset.sum_congr` `MulZeroClass.mul_zero` `Finset.sum_const_zero` `Fintype.sum_eq_zero_iff_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `LT.lt.le` `four_functions_theorem` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Pi.isOrderedRing` `mul_left_comm` `mul_comm` `sup_comm` `inf_comm` `mul_le_mul` `IsOrderedRing.toMulPosMono` `le_sup_left` `Finset.univ_infs_univ` `Finset.univ_sups_univ` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Fintype.sum_pos` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid`
`le_collapse_of_insert_mem` 📖	—	`Finset` `Finset.instMembership` `Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Finset.instInsert`	—	—	`collapse_eq` `le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `zero_add` `le_refl`
`le_collapse_of_mem` 📖	—	`Finset` `Finset.instMembership` `Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	—	`collapse_eq` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `add_zero` `le_refl`
`sum_collapse` 📖	mathematical	`Finset` `Finset.instHasSubset` `Finset.powerset` `Finset.instInsert` `Finset.instMembership`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`Finset.sum_ite_mem` `Finset.sum_image` `Set.InjOn.mono` `Finset.notMem_mono` `Finset.mem_powerset` `Set.LeftInvOn.injOn` `Finset.insert_erase_invOn` `Finset.sum_add_distrib` `Finset.sum_congr` `collapse_eq` `Finset.ext` `Finset.subset_insert_iff` `Finset.insert_subset_insert` `Finset.mem_insert_self` `Finset.insert_erase` `Finset.erase_ne_self` `Finset.sum_union` `Disjoint.mono` `inf_le_left` `disjoint_sdiff_self_right` `Finset.union_inter_distrib_right` `Finset.union_sdiff_of_subset` `Finset.powerset_mono` `Finset.subset_insert` `Finset.inter_eq_right`

---

← Back to Index