range_natCast

Mathlib.Topology.Instances.ENat

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

English

The image of the natural numbers inside ℕ∞ consists exactly of those elements strictly below ∞.

Русский

Образ натуральных чисел в ℕ∞ состоит ровно из элементов, меньше чем ∞.

LaTeX

$$$$\\operatorname{range}(\\uparrow: \\mathbb{N} \\to \\mathbb{N}_{\\infty}) = IIO^{+}(\\top).$$$$

Lean4

@[simp]
theorem range_natCast : range ((↑) : ℕ → ℕ∞) = Iio ⊤ :=
  WithTop.range_coe

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

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

Разделы

Аффилиация

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