not_isBot

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#not_isBot

English

In a type with NoBotOrder, no element is bottom; i.e., for every a, there exists x with x < a.

Русский

В типе с NoBotOrder ни один элемент не является нижним, то есть для каждого a существует x < a.

LaTeX

$$$\forall a \in \alpha:\, \neg \mathrm{IsBot}(a)$$$

Lean4

@[simp]
theorem not_isBot [NoBotOrder α] (a : α) : ¬IsBot a := fun h =>
  let ⟨_, hb⟩ := exists_not_ge a
  hb <| h _

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

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

Разделы

Аффилиация

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