untop_le_iff

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.untop_le_iff

English

If hy is a non-top proof, then a ≤ y.untop hy iff a ≤ y in WithTop(α).

Русский

Если hy — доказательство не-верхности, то a ≤ y.untop hy эквивалентно a ≤ y в WithTop(α).

LaTeX

$$$(hy : y \neq \top) \Rightarrow (a \le y.untop hy) \iff (a \le y)$$$

Lean4

theorem untop_le_iff (hx : x ≠ ⊤) : untop x hx ≤ b ↔ x ≤ b := by lift x to α using id hx; simp

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

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

Разделы

Аффилиация

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