compl_image_set_of — Mathlib

English

For any property p on subsets, the image under complement of the set {s | p(s)} equals {s | p(s^c)}.

Русский

Для любой свойства p над подмножествами верно: образ подмножества по операции комплемента равен подмножеству {s | p(s^c)}.

LaTeX

$$$\\mathrm{compl}''\\{s \\mid p(s)\\} = \\{s \\mid p(s^{c})\\}$$$

Lean4

theorem compl_image_set_of {p : Set α → Prop} : compl '' {s | p s} = {s | p sᶜ} :=
  congr_fun compl_image p

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