preimage — Mathlib

English

If f is an involution on α, then the preimage operator with respect to f is an involution on the power set of α: for every subset s, Set.preimage f (Set.preimage f s) = s.

Русский

Если f — инволютивное отображение на α, то операция взятия предобраза по f дважды равна тождественному отображению на множестве подмножеств α.

LaTeX

$$$ \forall S \subseteq \alpha, \operatorname{Set.preimage} f (\operatorname{Set.preimage} f S) = S $$$

Lean4

protected theorem preimage {f : α → α} (hf : Involutive f) : Involutive (preimage f) :=
  hf.rightInverse.preimage_preimage

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