homOfLE_comp — Mathlib

English

Composition of homs corresponds to transitivity of inequalities: homOfLE h followed by homOfLE k equals homOfLE (h trans k).

Русский

Сложение морфизмов соответствует транспозиции неравенств: homOfLE h затем homOfLE k равно homOfLE (h trans k).

LaTeX

$$$\mathrm{homOfLE}(h) \circ \mathrm{homOfLE}(k) = \mathrm{homOfLE}(\mathsf{trans}(h,k)).$$$

Lean4

@[simp]
theorem homOfLE_comp {x y z : X} (h : x ≤ y) (k : y ≤ z) : homOfLE h ≫ homOfLE k = homOfLE (h.trans k) :=
  rfl

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