on_preimage — Mathlib

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

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