continuous_precomp — Mathlib

English

For a fixed morphism f: A ⟶ B, the precomposition map (f ≫ ·): (B ⟶ R) → (A ⟶ R) is continuous.

Русский

Для фиксированного отображения f: A ⟶ B отображение предосогласования (f ≫ ·): (B ⟶ R) → (A ⟶ R) непрерывно.

LaTeX

$$$\text{Continuous}$ (f \gg\cdot) : (B \to R) \to (A \to R) $$$$

Lean4

@[fun_prop]
theorem continuous_precomp (f : A ⟶ B) : Continuous ((f ≫ ·) : (B ⟶ R) → (A ⟶ R)) :=
  continuous_induced_rng.mpr ((Pi.continuous_precomp f.hom).comp continuous_induced_dom)

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