one_le_cast

Mathlib.Data.Num.Lemmas

URI: https://scilib.ai/kg/mathlib#PosNum.one_le_cast

← MathLib Explorer

English

0 < (n : α) for any PosNum n (under appropriate structure).

Русский

0 < (n : α) для любого PosNum n (при условии нужной структуры).

LaTeX

$$$ 0 < (n : \alpha) $$$

Lean4

@[simp]
theorem one_le_cast [Semiring α] [PartialOrder α] [IsStrictOrderedRing α] (n : PosNum) : (1 : α) ≤ n := by
  rw [← cast_to_nat, ← Nat.cast_one, Nat.cast_le (α := α)]; apply to_nat_pos

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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