continuous_map — Mathlib

English

The map from stdSimplex to stdSimplex induced by f is compatible with composition of maps.

Русский

Карта из stdSimplex в stdSimplex, индуцированная f, согласована с композицией отображений.

LaTeX

$$$\operatorname{stdSimplex.map}\; (g \circ f) = (\operatorname{stdSimplex.map}\; g) \circ (\operatorname{stdSimplex.map}\; f)$$$

Lean4

@[continuity]
theorem continuous_map [TopologicalSpace S] [IsTopologicalSemiring S] (f : X → Y) : Continuous (map (S := S) f) :=
  Continuous.subtype_mk ((FunOnFinite.continuous_linearMap S S f).comp continuous_induced_dom) _

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