map — Mathlib

English

Post-composition pushes forward locally constant maps: map(f,g) is the locally constant map x ↦ f(g(x)).

Русский

Постсочетование продвигает локально константные отображения: map(f,g) — локально константное отображение x ↦ f(g(x)).

LaTeX

$$$\\mathrm{map}(f,g) = \\langle f \\circ g, g.\\text{isLocallyConstant} \\circ f \\rangle$$$

Lean4

/-- Push forward of locally constant maps under any map, by post-composition. -/
def map (f : Y → Z) (g : LocallyConstant X Y) : LocallyConstant X Z :=
  ⟨f ∘ g, g.isLocallyConstant.comp f⟩

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