restrictLe₂_comp_restrictLe₂ — Mathlib

English

The composition of two restrictLe₂ maps corresponds to the transitive restriction.

Русский

Композицией двух restrictLe₂ можно получить ограничение по транзитивному отношению.

LaTeX

$$$(\\text{restrictLe}_2(a) \\circ \\text{restrictLe}_2(b)) = \\text{restrictLe}_2(a \\ \\text{trans}\\ b)$$$

Lean4

theorem restrictLe₂_comp_restrictLe₂ {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
    (restrictLe₂ (π := π) hab) ∘ (restrictLe₂ hbc) = restrictLe₂ (hab.trans hbc) :=
  rfl

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