mono

Mathlib.Order.Max

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

English

If a is maximal and a ≤ b then b is maximal.

Русский

Если a максимален и a ≤ b, то b максимален.

LaTeX

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

Lean4

theorem mono (ha : IsMax a) (h : a ≤ b) : IsMax b := fun _ hc => (ha <| h.trans hc).trans h

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

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

Разделы

Аффилиация

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