of_le_of_le'

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#WCovBy.of_le_of_le'

English

If a ⩿ c and a ≤ b ≤ c, then a ⩿ b.

Русский

Если a ⩿ c и a ≤ b ≤ c, то a ⩿ b.

LaTeX

$$$(a \\\\mathrel{\\\\trianglelefteq} c) \\\\land (a \\\\le b) \\\\land (b \\\\le c) \\\\Rightarrow a \\\\mathrel{\\\\trianglelefteq} b.$$$

Lean4

theorem of_le_of_le' (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : a ⩿ b :=
  ⟨hab, fun _x hax hxb ↦ hac.2 hax <| hxb.trans_le hbc⟩

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

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

Разделы

Аффилиация

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