le_coe_unbotD

Mathlib.Order.WithBot

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

English

For x ∈ WithBot α and b ∈ α, x ≤ x.unbotD b.

Русский

Для x ∈ WithBot α и b ∈ α, выполняется x ≤ x.unbotD b.

LaTeX

$$$ \text{For } x : WithBot\,\alpha,\; b : \alpha,\; x ≤ x.unbotD b $$$

Lean4

theorem le_coe_unbotD (x : WithBot α) (b : α) : x ≤ x.unbotD b := by cases x <;> simp

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

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

Разделы

Аффилиация

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