isMin

Mathlib.Order.Max

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

English

In a preorder α that is a subsingleton, every element a is minimal: IsMin a.

Русский

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

LaTeX

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

Lean4

protected theorem isMin (a : α) : IsMin a :=
  (Subsingleton.isBot _).isMin

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

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

Разделы

Аффилиация

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