continuous_delayReflLeft — Mathlib

English

The map p ↦ delayReflLeft(p.1, p.2) is continuous from I × Path x y to Path x y.

Русский

Карта (θ, γ) ↦ delayReflLeft(θ, γ) непрерывна.

LaTeX

$$continuous_delayReflLeft : Continuous fun p => Path.delayReflLeft p.fst p.snd$$

Lean4

theorem continuous_delayReflLeft : Continuous fun p : I × Path x y => delayReflLeft p.1 p.2 :=
  Path.continuous_symm.comp <|
    continuous_delayReflRight.comp <| continuous_fst.prodMk <| Path.continuous_symm.comp continuous_snd

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