coe_lt_one

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

For α with LT, (a : WithTop α) < 1 iff a < 1.

Русский

Для α с отношением <, (a : WithTop α) < 1 эквивалентно a < 1.

LaTeX

$$$(a : WithTop \alpha) < 1 \iff a < 1$$$

Lean4

@[to_additive (attr := simp, norm_cast) coe_lt_zero]
theorem coe_lt_one [LT α] {a : α} : (a : WithTop α) < 1 ↔ a < 1 :=
  coe_lt_coe

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

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

Разделы

Аффилиация

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