eqToHom_comp_homOfLE — Mathlib

English

If a = b and b ≤ c, then eqToHom(a=b) ≫ homOfLE(b ≤ c) = homOfLE(le_of_eq a=b.trans c).

Русский

Если a = b и b ≤ c, то eqToHom(a=b) ∘ homOfLE(b ≤ c) = homOfLE((a ≤ c) через преобразование).

LaTeX

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

Lean4

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

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