pred_top_lt_iff

Mathlib.Order.SuccPred.Basic

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

English

With NoMinOrder, pred ⊤ < a iff a = ⊤.

Русский

При NoMinOrder: pred ⊤ < a тогда и только тогда, когда a = ⊤.

LaTeX

$$$ \\operatorname{pred} \\top < a \\iff a = \\top $$$

Lean4

theorem pred_top_lt_iff [NoMinOrder α] : pred ⊤ < a ↔ a = ⊤ :=
  @lt_succ_bot_iff αᵒᵈ _ _ _ _ _

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

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

Разделы

Аффилиация

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