projRight — Mathlib

English

Projecting the product of two path-classes yields the first component, i.e., projLeft(prod q1 q2) = q1.

Русский

Проекция левой части продукции путевых классов дает первый компонент: projLeft(prod q1 q2) = q1.

LaTeX

$$$\mathrm{projLeft}(\mathrm{prod}\; q_1\; q_2) = q_1$$$

Lean4

/-- Abbreviation for projection onto the right coordinate of a path class. -/
abbrev projRight (p : Path.Homotopic.Quotient c₁ c₂) : Path.Homotopic.Quotient c₁.2 c₂.2 :=
  p.mapFn ⟨_, continuous_snd⟩

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