intersecting_iff_eq_empty_of_subsingleton

English

Let α be a type equipped with a meet operation and a bottom element, and assume α is a Subsingleton. Then a subset s of α is an intersecting family if and only if s is the empty set.

Русский

Пусть α — множество с операцией meet и нулем, и пусть α -- это пододнос. Тогда подмножество s ⊆ α является семейством с попарно непустым общим пересечением тогда и только тогда, когда s пусто.

LaTeX

$$$\mathrm{Intersecting}(s) \iff s = \emptyset$$$

Lean4

theorem intersecting_iff_eq_empty_of_subsingleton [Subsingleton α] (s : Set α) : s.Intersecting ↔ s = ∅ :=
  by
  refine
    subsingleton_of_subsingleton.intersecting.trans
      ⟨not_imp_comm.2 fun h => subsingleton_of_subsingleton.eq_singleton_of_mem ?_, ?_⟩
  · obtain ⟨a, ha⟩ := nonempty_iff_ne_empty.2 h
    rwa [Subsingleton.elim ⊥ a]
  · rintro rfl
    exact (Set.singleton_nonempty _).ne_empty.symm

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