on_preimage — Mathlib

English

Let g: δ → α and hf: IsMaxOn f s (g(b)). Then IsMaxOn (f ∘ g) (g^{-1}(s)) b.

Русский

Пусть g: δ → α и hf: IsMaxOn f s (g(b)). Тогда IsMaxOn (f ∘ g) (g^{-1}(s)) b.

LaTeX

$$$g : \delta \to \alpha\;{b : \delta}\;hf : IsMaxOn f s (g b) ⟹ IsMaxOn (f \circ g) (g^{-1}' s) b$$$

Lean4

theorem on_preimage (g : δ → α) {b : δ} (hf : IsMaxOn f s (g b)) : IsMaxOn (f ∘ g) (g ⁻¹' s) b :=
  hf.comp_tendsto (tendsto_principal_principal.mpr <| Subset.refl _)

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