intersecting_iff_pairwise_not_disjoint

English

Intersecting is equivalent to pairwise not disjointness plus the empty-set condition on the subfamily.

Русский

Пересекаемость эквивалентна попарному неразделению плюс условие пустого семейства.

LaTeX

$$$$\\text{Intersecting}(s) \\iff (s\\ Pairwise (\\lambda a b, \\lnot Disjoint(a,b))) \\land s \\neq {\\bot}$$$$

Lean4

theorem intersecting_iff_pairwise_not_disjoint : s.Intersecting ↔ (s.Pairwise fun a b => ¬Disjoint a b) ∧ s ≠ {⊥} :=
  by
  refine ⟨fun h => ⟨fun a ha b hb _ => h ha hb, ?_⟩, fun h a ha b hb hab => ?_⟩
  · rintro rfl
    exact intersecting_singleton.1 h rfl
  have := h.1.eq ha hb (Classical.not_not.2 hab)
  rw [this, disjoint_self] at hab
  rw [hab] at hb
  exact h.2 (eq_singleton_iff_unique_mem.2 ⟨hb, fun c hc => not_ne_iff.1 fun H => h.1 hb hc H.symm disjoint_bot_left⟩)

Похожие утверждения