exists_mem_finset — Mathlib

English

For a family 𝒜 of finite sets that is intersecting, and finite sets s,t ∈ 𝒜, there exists an a contained in both s and t.

Русский

Для семейства 𝒜 конечных множеств, являющегося пересекающим, и конечных множеств s,t ∈ 𝒜, существует элемент a, который принадлежит обоим s и t.

LaTeX

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

Lean4

theorem exists_mem_finset [DecidableEq α] {𝒜 : Set (Finset α)} (h𝒜 : 𝒜.Intersecting) {s t : Finset α} (hs : s ∈ 𝒜)
    (ht : t ∈ 𝒜) : ∃ a, a ∈ s ∧ a ∈ t :=
  not_disjoint_iff.1 <| disjoint_coe.not.2 <| h𝒜 hs ht

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