concatCM_left — Mathlib

English

On a left-anchored point x with hx the left-hand inclusion, the concatenation CM equals the left map component evaluated at x.

Русский

Для точки x слева при hx склейка CM равна левой компоненте отображения на x.

LaTeX

$$concatCM_left: with hx and fg, concatCM fg x = fg.1.1 ⟨x.1, x.2.1, hx⟩.$$

Lean4

@[simp]
theorem concatCM_left {x : Icc a c} (hx : x ≤ b) {fg : { fg : C(Icc a b, E) × C(Icc b c, E) // fg.1 ⊤ = fg.2 ⊥ }} :
    concatCM fg x = fg.1.1 ⟨x.1, x.2.1, hx⟩ := by exact concat_left fg.2 hx

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