zero_lt_coe

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#WithZero.zero_lt_coe

English

For every a ∈ α, the bottom element 0 is strictly less than the embedding of a in WithZero α.

Русский

Для каждого a ∈ α ноль строго меньше встраиваемого элемента a в WithZero α.

LaTeX

$$$ 0 < (a : \mathrm{WithZero} \alpha) $$$

Lean4

@[simp]
theorem zero_lt_coe (a : α) : 0 < (a : WithZero α) := by simp [lt_def]

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

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

Разделы

Аффилиация

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