lt_untopD_iff

Mathlib.Order.WithBot

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

English

For hy : y = ⊤ → a < b, we have a < y.untopD b ↔ a < y.

Русский

Для условия hy : y = ⊤ → a < b выполняется: a < y.untopD b ⇔ a < y.

LaTeX

$$$$ a < y.untopD(b) \\iff a < y \\quad \\text{(given } hy: y = \\top \\to a < b). $$$$

Lean4

theorem lt_untopD_iff (hy : y = ⊤ → a < b) : a < y.untopD b ↔ a < y := by cases y <;> simp [hy]

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

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

Разделы

Аффилиация

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