restrictLe₂_comp_restrictLe

Mathlib.Order.Restriction

URI: https://scilib.ai/kg/mathlib#Preorder.restrictLe₂_comp_restrictLe

English

The composition of restrictLe₂ with restrictLe equals restrictLe on the left endpoint.

Русский

Композиция restrictLe₂ с restrictLe равна restrictLe на левой границе.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru