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