mono

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#IsTop.mono

English

If a is the top and a ≤ b, then b is also top.

Русский

Если a — верхний элемент и a ≤ b, то b тоже верхний элемент.

LaTeX

$$$\\\\mathrm{IsTop}(a) \\\\rightarrow (a \\\\le b) \\\\rightarrow \\\\mathrm{IsTop}(b)$$$

Lean4

theorem mono (ha : IsTop a) (h : a ≤ b) : IsTop b := fun _ => (ha _).trans h

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

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

Разделы

Аффилиация

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