mem_compls — Mathlib

English

An element a belongs to the complemented set sᶜˢ if and only if its complement aᶜ belongs to s.

Русский

Элемент a принадлежит дополненному множеству sᶜˢ тогда и только тогда, когда его комплемент aᶜ принадлежит s.

LaTeX

$$$ a \\in s^{\\complement\\}\\!ˢ \\iff a^{\\complement} \\in s $$$

Lean4

@[simp]
theorem mem_compls : a ∈ sᶜˢ ↔ aᶜ ∈ s := by
  rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]

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