continuous_uncurry_iff — Mathlib

English

For any Y, the map g : Y → Path x y is continuous iff its uncurry is continuous.

Русский

Для любого Y отображение g: Y → Path x y непрерывно тогда и только тогда, когда его развёртывание (uncurry) непрерывно.

LaTeX

$$$ (\\text{Continuous}(\\text{Path.instHasUncurryPath.uncurry } g)) \\iff \\text{Continuous}(g) $$$

Lean4

theorem continuous_uncurry_iff {Y} [TopologicalSpace Y] {g : Y → Path x y} : Continuous ↿g ↔ Continuous g :=
  Iff.symm <|
    continuous_induced_rng.trans
      ⟨fun h => continuous_uncurry_of_continuous ⟨_, h⟩,
        continuous_of_continuous_uncurry (fun (y : Y) ↦ ContinuousMap.mk (g y))⟩

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