isMax

Mathlib.Order.Max

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

English

In a preorder α that is subsingleton, every element a is maximal: IsMax a.

Русский

В порядке α, являющемся субоднозначным, каждый элемент максимален: IsMax a.

LaTeX

$$$\\forall {\\alpha : Type*} [Preorder \\alpha] [Subsingleton \\alpha] (a : \\alpha), IsMax a$$$

Lean4

protected theorem isMax (a : α) : IsMax a :=
  (Subsingleton.isTop _).isMax

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

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

Разделы

Аффилиация

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