pred_coe_of_isMin

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#WithBot.pred_coe_of_isMin

English

If a is minimal, then pred(↑a) = ⊥ in WithBot.

Русский

Если a минимален, pred(↑a) = ⊥ в WithBot.

LaTeX

$$$$ \operatorname{pred}(\\uparrow a) = \\bot_{WithBot} $$$$

Lean4

@[simp]
theorem pred_coe_of_isMin {a : α} (h : IsMin a) : pred ↑a = (⊥ : WithBot α) :=
  dif_pos (pred_eq_iff_isMin.2 h)

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

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

Разделы

Аффилиация

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