preimage_comp — Mathlib

English

For any sets, the preimage of a set under the composition g ∘ f equals the preimage under f of the preimage under g of that set: (g ∘ f)^{-1}(s) = f^{-1}(g^{-1}(s)).

Русский

Для любых множеств выполняется: предобраз множества s под композициией g ∘ f равен предобразу под f от предобраза под g: (g ∘ f)^{-1}(s) = f^{-1}(g^{-1}(s)).

LaTeX

$$$ (g \\circ f)^{-1}(s) = f^{-1}(g^{-1}(s)). $$$

Lean4

theorem preimage_comp {s : Set γ} : g ∘ f ⁻¹' s = f ⁻¹' (g ⁻¹' s) :=
  rfl

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