continuous_sigma_map — Mathlib

English

A map from a sigma-type to a space X is continuous iff its restriction to each summand is continuous.

Русский

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

LaTeX

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

Lean4

@[simp 1100]
theorem continuous_sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} :
    Continuous (Sigma.map f₁ f₂) ↔ ∀ i, Continuous (f₂ i) :=
  continuous_sigma_iff.trans <| by simp only [Sigma.map, IsEmbedding.sigmaMk.continuous_iff, comp_def]

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