preimage_compl — Mathlib

English

If f is injective, the complement identity for preimages holds: preimage(sᶜ) = (preimage(s))ᶜ.

Русский

Если f инъективно, тогда выполняется тождество для дополнения предобраза: preimage(sᶜ) = (preimage(s))ᶜ.

LaTeX

$$$$ \\mathrm{preimage}(s^{\\mathrm{c}}, f) = (\\mathrm{preimage}(s,f))^{\\mathrm{c}}. $$$$

Lean4

theorem preimage_compl [DecidableEq α] [DecidableEq β] [Fintype α] [Fintype β] {f : α → β} (s : Finset β)
    (hf : Function.Injective f) : preimage sᶜ f hf.injOn = (preimage s f hf.injOn)ᶜ :=
  preimage_compl' _ _ _

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