cast_nonneg'

Mathlib.Data.Nat.Cast.Order.Basic

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

← MathLib Explorer

English

For every n ∈ ℕ, the image (n : α) is nonnegative: 0 ≤ (n : α).

Русский

Для каждого n ∈ ℕ образ (n : α) неотрицателен: 0 ≤ (n : α).

LaTeX

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

Lean4

/-- See also `Nat.cast_nonneg`, specialised for an `OrderedSemiring`. -/
@[simp low]
theorem cast_nonneg' (n : ℕ) : 0 ≤ (n : α) :=
  @Nat.cast_zero α _ ▸ mono_cast (Nat.zero_le n)

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

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

Разделы

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

Аффилиация

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