unbot_le_iff

Mathlib.Order.WithBot

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

English

If y ≠ ⊥, then a ≤ unbot(y) in α iff i(a) ≤ y in WithBot α.

Русский

Если y ≠ ⊥, тогда a ≤ unbot(y) в α эквивалентно i(a) ≤ y в WithBot α.

LaTeX

$$$ ( y \neq \bot ) \rightarrow ( a \le \mathrm{unbot}(y) \iff \iota(a) \le y ) $$$

Lean4

theorem unbot_le_iff (hx : x ≠ ⊥) : unbot x hx ≤ b ↔ x ≤ b := by lift x to α using id hx; simp

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

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

Разделы

Аффилиация

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