lt_coe_bot

Mathlib.Order.WithBot

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

English

For a x ∈ WithBot α, under OrderBot α, x < ⊥ in α corresponds to x = ⊥.

Русский

Для x ∈ WithBot α, при OrderBot α, x < ⊥ в α эквивалентно x = ⊥.

LaTeX

$$$ x < (\bot : \alpha) \iff x = \bot $$$

Lean4

@[simp]
theorem lt_coe_bot [OrderBot α] : x < (⊥ : α) ↔ x = ⊥ := by cases x <;> simp

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

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

Разделы

Аффилиация

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