compl_setOf_mem — Mathlib

English

The complement of {p : T.CompleteType α | φ ∈ p} equals {p : T.CompleteType α | φ.not ∈ p}.

Русский

Дополнение множества {p : T.CompleteType α | φ ∈ p} равно {p : T.CompleteType α | φ.not ∈ p}.

LaTeX

$$$ {p : T.CompleteType α | φ ∈ p}^{c} = {p : T.CompleteType α | φ.not ∈ p}$$$

Lean4

@[simp]
theorem compl_setOf_mem {φ : L[[α]].Sentence} : {p : T.CompleteType α | φ ∈ p}ᶜ = {p : T.CompleteType α | φ.not ∈ p} :=
  ext fun _ => (not_mem_iff _ _).symm

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