one_lt_coe

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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