frestrictLe₂_comp_frestrictLe₂

English

The two-step restriction composes to a single restriction with transitive bound.

Русский

Две последовательные операции ограничения дают одно ограничение с переходом по отношению.

LaTeX

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

Lean4

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

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