Documentation Verification Report

Intersecting

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

Statistics

Metric	Count
Definitions `Intersecting`, `IsIntersectingOf`	2
Theorems `bot_notMem`, `card_le`, `compl_notMem`, `disjoint_map_compl`, `exists_card_eq`, `exists_mem_finset`, `exists_mem_set`, `insert`, `isUpperSet`, `isUpperSet'`, `is_max_iff_card_eq`, `mono`, `ne_bot`, `notMem`, `anti`, `empty`, `mono`, `univ`, `intersecting`, `intersecting_empty`, `intersecting_iff_eq_empty_of_subsingleton`, `intersecting_iff_pairwise_not_disjoint`, `intersecting_insert`, `intersecting_singleton`	24
Total	26

Set

Definitions

Name	Category	Theorems
`Intersecting` 📖	MathDef	9 math math: `intersecting_empty`, `intersecting_iff_eq_empty_of_subsingleton`, `intersecting_iff_pairwise_not_disjoint`, `Subsingleton.intersecting`, `intersecting_insert`, `intersecting_singleton`, `Intersecting.mono`, `Intersecting.exists_card_eq`, `Intersecting.insert`
`IsIntersectingOf` 📖	MathDef	4 math math: `IsIntersectingOf.mono`, `IsIntersectingOf.empty`, `IsIntersectingOf.univ`, `IsIntersectingOf.anti`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intersecting_empty` 📖	mathematical	—	`Intersecting` `Set` `instEmptyCollection`	—	—
`intersecting_iff_eq_empty_of_subsingleton` 📖	mathematical	—	`Intersecting` `Set` `instEmptyCollection`	—	`Subsingleton.intersecting` `subsingleton_of_subsingleton` `not_imp_comm` `Subsingleton.eq_singleton_of_mem` `nonempty_iff_ne_empty` `Nonempty.ne_empty` `singleton_nonempty`
`intersecting_iff_pairwise_not_disjoint` 📖	mathematical	—	`Intersecting` `Pairwise` `Disjoint` `SemilatticeInf.toPartialOrder`	—	`intersecting_singleton` `Pairwise.eq` `eq_singleton_iff_unique_mem` `disjoint_self` `not_ne_iff` `disjoint_bot_left`
`intersecting_insert` 📖	mathematical	—	`Intersecting` `Set` `instInsert` `Disjoint` `SemilatticeInf.toPartialOrder`	—	`Intersecting.mono` `subset_insert` `Intersecting.ne_bot` `mem_insert` `mem_insert_of_mem` `Intersecting.insert`
`intersecting_singleton` 📖	mathematical	—	`Intersecting` `Set` `instSingletonSet`	—	—

Set.Intersecting

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_notMem` 📖	mathematical	`Set.Intersecting`	`Set` `Set.instMembership` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`disjoint_bot_left`
`card_le` 📖	mathematical	`Set.Intersecting` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.card` `Fintype.card`	—	`LE.le.trans_eq'` `compl_injective` `disjoint_map_compl` `Finset.card_le_univ` `Finset.card_disjUnion` `Finset.card_map`
`compl_notMem` 📖	mathematical	`Set.Intersecting` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Set` `Set.instMembership`	`Set` `Set.instMembership` `Compl.compl` `BooleanAlgebra.toCompl`	—	`disjoint_compl_right`
`disjoint_map_compl` 📖	mathematical	`Set.Intersecting` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `SetLike.coe` `Finset` `Finset.instSetLike`	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `Finset.map` `Compl.compl` `BooleanAlgebra.toCompl` `compl_injective`	—	`compl_injective` `Finset.disjoint_left` `Finset.mem_map` `compl_notMem`
`exists_card_eq` 📖	mathematical	`Set.Intersecting` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset` `Finset.instHasSubset` `Finset.card` `Fintype.card` `Set.Intersecting` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `SetLike.coe` `Finset.instSetLike`	—	`card_le` `Set.Subset.rfl` `is_max_iff_card_eq` `Mathlib.Tactic.Push.not_forall_eq` `HasSubset.Subset.trans` `Finset.instIsTransSubset` `ssubset_iff_subset_ne` `Finset.instIsNonstrictStrictOrderSubsetSSubset` `Finset.instAntisymmSubset`
`exists_mem_finset` 📖	mathematical	`Set.Intersecting` `Finset` `Lattice.toSemilatticeInf` `Finset.instLattice` `Finset.instOrderBot` `Set` `Set.instMembership`	`Finset` `SetLike.instMembership` `Finset.instSetLike`	—	`Set.not_disjoint_iff` `Iff.not` `Finset.disjoint_coe`
`exists_mem_set` 📖	mathematical	`Set.Intersecting` `Set` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Set.instMembership`	`Set` `Set.instMembership`	—	`Set.not_disjoint_iff`
`insert` 📖	mathematical	`Set.Intersecting` `Disjoint` `SemilatticeInf.toPartialOrder`	`Set.Intersecting` `Set` `Set.instInsert`	—	`disjoint_self` `Disjoint.symm`
`isUpperSet` 📖	mathematical	`Set.Intersecting`	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`insert` `eq_bot_mono` `ne_bot` `Disjoint.mono_left` `Set.subset_insert` `Set.mem_insert`
`isUpperSet'` 📖	mathematical	`Set.Intersecting` `SetLike.coe` `Finset` `Finset.instSetLike`	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.coe_insert` `insert` `eq_bot_mono` `ne_bot` `Disjoint.mono_left` `Finset.subset_insert` `Finset.mem_insert_self`
`is_max_iff_card_eq` 📖	mathematical	`Set.Intersecting` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.card` `Fintype.card`	—	`compl_injective` `disjoint_map_compl` `Finset.coe_eq_univ` `Finset.disjUnion_eq_union` `Finset.coe_union` `Finset.coe_map` `Set.image_eq_preimage_of_inverse` `compl_compl` `Set.eq_univ_of_forall` `Finset.ne_insert_of_notMem` `Finset.coe_insert` `insert` `Finset.coe_singleton` `Set.intersecting_singleton` `top_ne_bot` `Finset.singleton_ne_empty` `Finset.coe_eq_empty` `IsUpperSet.top_notMem` `isUpperSet'` `compl_bot` `Finset.empty_subset` `Disjoint.le_compl_left` `Finset.subset_insert` `Fintype.card.eq_1` `Finset.card_disjUnion` `Finset.card_map` `Finset.eq_of_subset_of_card_le` `LE.le.trans_eq` `card_le`
`mono` 📖	mathematical	`Set` `Set.instHasSubset` `Set.Intersecting`	`Set.Intersecting`	—	—
`ne_bot` 📖	—	`Set.Intersecting` `Set` `Set.instMembership`	—	—	`bot_notMem`
`notMem` 📖	mathematical	`Set.Intersecting` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Set` `Set.instMembership` `Compl.compl` `BooleanAlgebra.toCompl`	`Set` `Set.instMembership`	—	`disjoint_compl_left`

Set.IsIntersectingOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	mathematical	`Set` `Finset` `Set.instHasSubset` `Set.IsIntersectingOf`	`Set.IsIntersectingOf`	—	`Set.Pairwise.mono`
`empty` 📖	mathematical	—	`Set.IsIntersectingOf` `Set` `Finset` `Set.instEmptyCollection`	—	—
`mono` 📖	mathematical	`Set` `Set.instHasSubset` `Set.IsIntersectingOf`	`Set.IsIntersectingOf`	—	—
`univ` 📖	mathematical	—	`Set.IsIntersectingOf` `Set.univ`	—	`Set.pairwise_of_forall`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intersecting` 📖	mathematical	`Set.Subsingleton`	`Set.Intersecting`	—	`Set.intersecting_iff_pairwise_not_disjoint` `pairwise`

---

← Back to Index