isMax

Mathlib.Order.Max

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

English

If an element a is the top of a partially ordered set, then a is a maximal element.

Русский

Если элемент a является верхним элементом частично упорядоченного множества, то он является максимальным элементом.

LaTeX

$$$\\\\mathrm{IsTop}(a) \\\\rightarrow \\\\mathrm{IsMax}(a)$$$

Lean4

protected theorem isMax (h : IsTop a) : IsMax a := fun b _ => h b

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

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

Разделы

Аффилиация

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