Theorems · Theorem · combinatorics

Set.Intersecting.is_max_iff_card_eq

∀ {α : Type u_1} [inst : BooleanAlgebra α] [Nontrivial α] [inst_2 : Fintype α] {s : Finset α},
  (↑s).Intersecting → ((∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t) ↔ 2 * s.card = Fintype.card α)

Defined in: Mathlib.Combinatorics.SetFamily.Intersecting
Cited by: 2 results in Mathlib
Foundations: Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: BooleanAlgebra Nontrivial Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites48

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

Setproof · cited by 53,352
Finsetstatement and proof · cited by 13,712
Top.topproof · cited by 9,680
SetLike.coestatement and proof · cited by 8,199
Fintypestatement and proof · cited by 7,736
Set.imageproof · cited by 5,609
Set.preimageproof · cited by 4,946
Bot.botproof · cited by 4,720
Set.univproof · cited by 3,945
Finset.univproof · cited by 3,473
Compl.complproof · cited by 2,925
Nontrivialstatement and proof · cited by 2,416

Cited by2

Results whose statement or proof uses this declaration.

Set.Intersecting.exists_card_eqproof · cited by 1
Finset.card_biUnion_le_of_intersectingproof · cited by 0