snd_lineMap — Mathlib

English

The line map on a product space acts componentwise with respect to the projections.

Русский

LineMap на произведении действует по компонентам через проекции.

LaTeX

$$$ (\text{fst} \circ \text{lineMap})(p_0,p_1) = \text{lineMap}(p_0.1, p_1.1) $ and $ (\text{snd} \circ \text{lineMap})(p_0,p_1) = \text{lineMap}(p_0.2, p_1.2) $$$

Lean4

@[simp]
theorem snd_lineMap (p₀ p₁ : P1 × P2) (c : k) : (lineMap p₀ p₁ c).2 = lineMap p₀.2 p₁.2 c :=
  snd.apply_lineMap p₀ p₁ c

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