cast_pos'

Mathlib.Data.Nat.Cast.Order.Basic

URI: https://scilib.ai/kg/mathlib#Nat.cast_pos'

← MathLib Explorer

English

For all n, 0 < (n : α) iff 0 < n.

Русский

Для всех n верно: 0 < (n : α) тогда и только тогда, когда 0 < n.

LaTeX

$$$\forall n \in \mathbb{N},\ 0 < (n : \alpha) \iff 0 < n.$$$

Lean4

/-- See also `Nat.cast_pos`, specialised for an `OrderedSemiring`. -/
@[simp low]
theorem cast_pos' {n : ℕ} : (0 : α) < n ↔ 0 < n := by cases n <;> simp [cast_add_one_pos]

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

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

Разделы

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

Аффилиация

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