continuous_toTopMap — Mathlib

English

The construction toTopMap is continuous with respect to the topologies on x.toTopObj and y.toTopObj.

Русский

Конструкция toTopMap непрерывна относительно топологий на x.toTopObj и y.toTopObj.

LaTeX

$$$\\text{Continuous}(\\mathrm{toTopMap}(f))$ for all morphisms f in SimplexCategory$$

Lean4

@[continuity, fun_prop]
theorem continuous_toTopMap {x y : SimplexCategory} (f : x ⟶ y) : Continuous (toTopMap f) :=
  by
  refine Continuous.subtype_mk (continuous_pi fun i => ?_) _
  dsimp only [coe_toTopMap]
  exact continuous_finset_sum _ (fun j _ => (continuous_apply _).comp continuous_subtype_val)

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