Theorems · Theorem · combinatorics
Set.Intersecting.insert
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s : Set α} {a : α},
s.Intersecting → a ≠ ⊥ → (∀ b ∈ s, ¬Disjoint a b) → (insert a s).Intersecting- Cited by
- 4 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext
- Assumes
- SemilatticeInfOrderBot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Bot.botstatement and proof · cited by 4,720
- Disjointstatement and proof · cited by 2,201
- OrderBotstatement and proof · cited by 1,055
- SemilatticeInfstatement and proof · cited by 634
- Disjoint.symmproof · cited by 125
- disjoint_selfproof · cited by 28
- Set.Intersectingstatement and proof · cited by 22
Cited by4
Results whose statement or proof uses this declaration.
- Set.Intersecting.is_max_iff_card_eqproof · cited by 2
- Set.Intersecting.isUpperSet'proof · cited by 2
- Set.Intersecting.isUpperSetproof · cited by 0
- Set.intersecting_insertproof · cited by 0