concatCM_right — Mathlib

English

Symmetrically, with hx on the right boundary, the concatenation CM equals the right map component evaluated at x.

Русский

Симметрично, на правой границе, склейка CM равна правой компоненте отображения на x.

LaTeX

$$concatCM_right: with hx, concatCM fg x = fg.1.2 ⟨x.1, hx, x.2.2⟩.$$

Lean4

@[simp]
theorem concatCM_right {x : Icc a c} (hx : b ≤ x) {fg : { fg : C(Icc a b, E) × C(Icc b c, E) // fg.1 ⊤ = fg.2 ⊥ }} :
    concatCM fg x = fg.1.2 ⟨x.1, hx, x.2.2⟩ :=
  concat_right fg.2 hx

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