homOfLE_comp_eqToHom — Mathlib

English

Compositions of homOfLE with eqToHom satisfy a compatibility: composing with eqToHom(b=c) equals homOfLE(a ≤ c).

Русский

Сочетания homOfLE и eqToHom удовлетворяют совместимости: компоновка с eqToHom(b=c) равна homOfLE(a ≤ c).

LaTeX

$$$\mathrm{homOfLE\_comp\_eqToHom} : \forall a b c, \; (hab : a \le b) (hbc : b = c) \\quad \mathrm{eqToHom}\,hbc \; \circ \mathrm{homOfLE}(hab) = \mathrm{homOfLE}(hab.trans (\mathrm{le\_of\_eq}\, hbc)).$$$

Lean4

@[simp, reassoc]
theorem homOfLE_comp_eqToHom {a b c : X} (hab : a ≤ b) (hbc : b = c) :
    homOfLE hab ≫ eqToHom hbc = homOfLE (hab.trans (le_of_eq hbc)) :=
  rfl

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