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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring sum Finset NonUnitalNonAssocSemiring.toAddCommMonoid HasInfs.infs hasInfs decidableEq instLattice HasSups.sups hasSups Lattice.toSemilatticeSup	—	induction MulZeroClass.mul_zero sum_congr infs_empty sups_empty instReflLe 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 SetLike.instMembership Finset.instSetLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset SetLike.instMembership Finset.instSetLike 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 SetLike.instMembership Finset.instSetLike 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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring HasInfs.infs Finset Finset.hasInfs Finset.decidableEq Finset.instLattice Finset.instInter HasSups.sups Finset.hasSups Lattice.toSemilatticeSup Finset.instUnion	—	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 📖	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	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 SetLike.instMembership Finset.instSetLike 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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring 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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid HasInfs.infs Finset Finset.hasInfs HasSups.sups Finset.hasSups Lattice.toSemilatticeSup	—	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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ	—	Finset.sum_congr Finset.univ_infs_univ Finset.univ_sups_univ four_functions_theorem
holley 📖	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 Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SemilatticeInf.toMin SemilatticeSup.toMax Lattice.toSemilatticeSup	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	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 instReflLe 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 📖	mathematical	Finset SetLike.instMembership Finset.instSetLike 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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 📖	mathematical	Finset SetLike.instMembership Finset.instSetLike 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	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	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 SetLike.instMembership Finset.instSetLike	Finset.sum Finset NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.powerset	—	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