continuous_sigma_iff — Mathlib

English

For any i, preimage of the singleton {i} under Sigma.fst equals the range of Sigma.mk i.

Русский

Для каждого i предобраз единичного множества {i} под Sigma.fst равен образу Sigma.mk i.

LaTeX

$$$\\operatorname{preimage}(\\Sigma.fst)(\\{i\\}) = \\operatorname{range}(\\Sigma.mk i)$$$

Lean4

/-- A map out of a sum type is continuous iff its restriction to each summand is. -/
@[simp]
theorem continuous_sigma_iff {f : Sigma σ → X} : Continuous f ↔ ∀ i, Continuous fun a => f ⟨i, a⟩ :=
  by
  delta instTopologicalSpaceSigma
  rw [continuous_iSup_dom]
  exact forall_congr' fun _ => continuous_coinduced_dom

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