pred_top_le_iff

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.pred_top_le_iff

English

pred ⊤ ≤ a iff a = ⊤ or a = pred ⊤.

Русский

pred ⊤ ≤ a эквивалентно a = ⊤ или a = pred ⊤.

LaTeX

$$$ pred\\top \\le a \\iff a = \\top \\lor a = pred\\top $$$

Lean4

theorem pred_top_le_iff : pred ⊤ ≤ a ↔ a = ⊤ ∨ a = pred ⊤ :=
  @le_succ_bot_iff αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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