eq_top_iff_forall_gt

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.eq_top_iff_forall_gt

English

In a Preorder α without top restrictions, y = ⊤ iff ∀ a: α, a < y.

Русский

В предпорядке без ограничений на вершину, y = ⊤ тогда, когда для всех a ∈ α верно a < y.

LaTeX

$$$$ y = \\top \\iff \\forall a: \\alpha, a < y. $$$$

Lean4

theorem eq_top_iff_forall_gt : y = ⊤ ↔ ∀ a : α, a < y := by cases y <;> simp; simpa using ⟨_, lt_irrefl _⟩

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

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

Разделы

Аффилиация

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