map_natCast_nonneg

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.map_natCast_nonneg

English

For any ENat n, the image under Nat.cast is nonnegative: 0 ≤ n.map (Nat.cast : ℕ → α).

Русский

Для любого n ∈ ENat образ под Nat.cast в α неотрицателен: 0 ≤ n.map Nat.cast.

LaTeX

$$$$ 0 \\le (\\mathrm{ENat.map}(\\mathrm{Nat.cast}: \\mathbb{N} \\to \\alpha))(n) $$$$

Lean4

@[simp]
theorem map_natCast_nonneg : 0 ≤ n.map (Nat.cast : ℕ → α) := by cases n <;> simp

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

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

Разделы

Аффилиация

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