isBot

Mathlib.Order.Directed

URI: https://scilib.ai/kg/mathlib#IsMin.isBot

English

In a directed setting, a minimal element cannot be maximal.

Русский

В направленной системе минимальный элемент не может быть максимальным.

LaTeX

$$$IsMin(b) \rightarrow \lnot IsMax(b)$$$

Lean4

protected theorem isBot [IsDirected α (· ≥ ·)] (h : IsMin a) : IsBot a := fun b =>
  let ⟨_, hca, hcb⟩ := exists_le_le a b
  (h hca).trans hcb

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

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

Разделы

Аффилиация

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