symm_continuous_family — Mathlib

English

If γ is a family of paths parameterized by ι and continuous in the uncurry sense, then the family t ↦ (γ t).symm is continuous.

Русский

Если γ — семейство путей, параметризованное по ι, и непрерывно как функция, то t ↦ (γ t).symm непрерывно.

LaTeX

$$Continuous (fun t => (γ t).symm) given Continuous γ$$

Lean4

@[continuity, fun_prop]
theorem symm_continuous_family {ι : Type*} [TopologicalSpace ι] {a b : ι → X} (γ : ∀ t : ι, Path (a t) (b t))
    (h : Continuous ↿γ) : Continuous ↿fun t => (γ t).symm :=
  h.comp (continuous_id.prodMap continuous_symm)

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