compl_notMem — Mathlib

English

In a Boolean algebra, if s is intersecting and a ∈ s, then the complement a^c is not in s.

Русский

В булевой алгебре, если s является intersecting и a ∈ s, тогда комплемент a^c не принадлежит s.

LaTeX

$$$\text{Intersecting}(s) \land a \in s \Rightarrow a^{\complement} \notin s$$$

Lean4

theorem compl_notMem {s : Set α} (hs : s.Intersecting) {a : α} (ha : a ∈ s) : aᶜ ∉ s := fun h =>
  hs ha h disjoint_compl_right

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