not_coe_le_bot

Mathlib.Order.WithBot

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

English

For a ∈ α, not (a : WithBot α) ≤ ⊥.

Русский

Для a ∈ α не выполняется a ≤ ⊥ в WithBot α.

LaTeX

$$$a \;\nrightarrow\; (a : WithBot α) \le ⊥$$$

Lean4

theorem not_coe_le_bot (a : α) : ¬(a : WithBot α) ≤ ⊥ := by simp [le_def]

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

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

Разделы

Аффилиация

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