continuous_delayReflRight — Mathlib

English

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

Русский

Карта (θ, γ) ↦ delayReflRight(θ, γ) непрерывна по отношению к I × Path(x, y) в Path(x, y).

LaTeX

$$continuous_delayReflRight : Continuous fun p : I × Path x y => delayReflRight p.1 p.2$$

Lean4

theorem continuous_delayReflRight : Continuous fun p : I × Path x y => delayReflRight p.1 p.2 :=
  continuous_uncurry_iff.mp <|
    (continuous_snd.comp continuous_fst).eval <|
      continuous_qRight.comp <| continuous_snd.prodMk <| continuous_fst.comp continuous_fst

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