isMin

Mathlib.Order.Max

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

English

If a is a bottom element, then a is a minimum element.

Русский

Если элемент является нижним, то он является минимальным.

LaTeX

$$$\mathrm{IsBot}(a) \Rightarrow \mathrm{IsMin}(a)$$$

Lean4

protected theorem isMin (h : IsBot a) : IsMin a := fun b _ => h b

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

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

Разделы

Аффилиация

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