exists_mem_set — Mathlib

English

If a family 𝒜 of sets is intersecting, and s,t ∈ 𝒜, then there exists an element a ∈ s ∩ t.

Русский

Если семейство 𝒜 парно пересекающихся множеств, и s,t ∈ 𝒜, то существует элемент a, лежащий в s ∩ t.

LaTeX

$$$\exists a \; (a \in s \land a \in t)$$$

Lean4

theorem exists_mem_set {𝒜 : Set (Set α)} (h𝒜 : 𝒜.Intersecting) {s t : Set α} (hs : s ∈ 𝒜) (ht : t ∈ 𝒜) :
    ∃ a, a ∈ s ∧ a ∈ t :=
  not_disjoint_iff.1 <| h𝒜 hs ht

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