map_f — Mathlib

English

The map component of a SingularManifold under a continuous φ preserves the defining function: the function component after map equals φ composed with the original f.

Русский

Компонента функции Manifold после отображения по непрерывному φ сохраняет исходную функцию: f после отображения равна φ ∘ f.

LaTeX

$$$ (s.map hφ).f = φ \\circ s.f $$$

Lean4

@[simp, mfld_simps]
theorem map_f (s : SingularManifold X k I) {φ : X → Y} (hφ : Continuous φ) : (s.map hφ).f = φ ∘ s.f :=
  rfl

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