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