Mathlib Map

Theorems · Definition · combinatorics

Set.Intersecting

{α : Type u_1} → [inst : SemilatticeInf α] → [OrderBot α] → Set α → Prop

A set family is intersecting if every pair of elements is non-disjoint.

Defined in
Mathlib.Combinatorics.SetFamily.Intersecting
Cited by
22 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
SemilatticeInfOrderBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.Intersecting.insert · cited by 4Intersecting.insertSet.Intersecting.ne_bot · cited by 4Intersecting.ne_botSet.Intersecting.card_le · cited by 3Intersecting.card_leSet.Intersecting.disjoint_map_compl · cited by 2Intersecting.disjoint_map…Set.Intersecting.isUpperSet' · cited by 2Intersecting.isUpperSet'Set.Intersecting.is_max_iff_card_eq · cited by 2Intersecting.is_max_iff_c…Set.intersecting_singleton · cited by 2Set.intersecting_singletonSet.Intersecting.bot_notMem · cited by 1Intersecting.bot_notMemSet.Intersecting.compl_notMem · cited by 1Intersecting.compl_notMemSet.Intersecting.exists_card_eq · cited by 1Intersecting.exists_card_…Set.Intersecting.mono · cited by 1Intersecting.monoSet.intersecting_iff_pairwise_not_disjoint · cited by 1Set.intersecting_iff_pair…Set.Subsingleton.intersecting · cited by 1Subsingleton.intersectingFinset.erdos_ko_rado · cited by 0Finset.erdos_ko_radoSet.Intersecting.exists_mem_finset · cited by 0Intersecting.exists_mem_f…Set · cited by 53352SetDisjoint · cited by 2201DisjointOrderBot · cited by 1055OrderBotSemilatticeInf · cited by 634SemilatticeInfSet.IntersectingCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Disjointproof · cited by 2,201
  • OrderBotstatement and proof · cited by 1,055
  • SemilatticeInfstatement and proof · cited by 634

Cited by22

Results whose statement or proof uses this declaration.