English
Let g: δ → α and hf: IsExtrOn f s (g(b)). Then IsExtrOn (f ∘ g) (g^{-1}' s) b.
Русский
Пусть g: δ → α и hf: IsExtrOn f s (g(b)). Тогда IsExtrOn (f ∘ g) (g^{-1}' s) b.
LaTeX
$$$g : \delta \to \alpha\;{b : \delta}\;hf : IsExtrOn f s (g b) ⟹ IsExtrOn (f \circ g) (g^{-1}' s) b$$$
Lean4
theorem on_preimage (g : δ → α) {b : δ} (hf : IsExtrOn f s (g b)) : IsExtrOn (f ∘ g) (g ⁻¹' s) b :=
hf.elim (fun hf => (hf.on_preimage g).isExtr) fun hf => (hf.on_preimage g).isExtr