mem_compl_image — Mathlib

English

For a Boolean algebra α and element t, t belongs to the complement-image of s iff t complement belongs to s: t ∈ compl'' s ↔ t^c ∈ s.

Русский

Для булевой алгебры α и элемента t: t принадлежит образу дополнения множества s тогда и только тогда, когда t^c принадлежит s.

LaTeX

$$$ t \\in \\text{compl}'' s \\ \\Leftrightarrow \\ t^c \\in s. $$$

Lean4

theorem mem_compl_image [BooleanAlgebra α] (t : α) (s : Set α) : t ∈ HasCompl.compl '' s ↔ tᶜ ∈ s := by
  simp [← preimage_compl_eq_image_compl]

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