ge_of_gt

Mathlib.Order.Cover

URI: https://scilib.ai/kg/mathlib#WCovBy.ge_of_gt

English

If a ⋖ b and a < c, then b ≤ c.

Русский

Если a ⋖ b и a < c, тогда b ≤ c.

LaTeX

$$a \mathrm{CovBy} b \rightarrow a < c \rightarrow b \le c$$

Lean4

theorem ge_of_gt (hab : a ⩿ b) (hac : a < c) : b ≤ c :=
  not_lt.1 <| hab.2 hac

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

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

Разделы

Аффилиация

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