preimage_comp_eq — Mathlib

English

For functions f: α → β and g: β → γ and any set s ⊆ γ, the preimage under g ∘ f equals the preimage under f of the preimage under g of s: preimage (g ∘ f)(s) = preimage f (preimage g (s)).

Русский

Для функций f: α → β и g: β → γ и любого множества s ⊆ γ имеет место: (g ∘ f)^{-1}(s) = f^{-1}(g^{-1}(s)).

LaTeX

$$$ \\operatorname{preimage}(g \\circ f) = \\operatorname{preimage}(f) \\circ \\operatorname{preimage}(g). $$$

Lean4

theorem preimage_comp_eq : preimage (g ∘ f) = preimage f ∘ preimage g :=
  rfl

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