le_unbot_iff

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithBot.le_unbot_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 le_unbot_iff (hy : y ≠ ⊥) : a ≤ unbot y hy ↔ a ≤ y := by lift y to α using id hy; simp

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

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

Разделы

Аффилиация

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