continuous_sigma — Mathlib

English

A sigma-type map is continuous if and only if its restriction to each summand is continuous.

Русский

Отображение из сигма-типа непрерывно тогда и только тогда, когда его ограничение на каждую компоненту непрерывно.

LaTeX

$$$\\text{Continuous}(f) \\iff \\forall i, \\ \\text{Continuous}(\\lambda a. f(\\langle i,a\\rangle))$$$

Lean4

/-- A map out of a sum type is continuous if its restriction to each summand is. -/
@[continuity, fun_prop]
theorem continuous_sigma {f : Sigma σ → X} (hf : ∀ i, Continuous fun a => f ⟨i, a⟩) : Continuous f :=
  continuous_sigma_iff.2 hf

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