isOpenEmbedding_natCast

Mathlib.Topology.Instances.ENat

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

English

The embedding Nat → ℕ∞ is an open embedding: it is an embedding and its image is open.

Русский

Встраивание Nat → ℕ∞ есть открытое вложение: образ открыт.

LaTeX

$$$$\\text{IsOpenEmbedding}(\\uparrow: \\mathbb{N} \\to \\mathbb{N}_{\\infty}).$$$$

Lean4

theorem isOpenEmbedding_natCast : IsOpenEmbedding ((↑) : ℕ → ℕ∞) :=
  ⟨isEmbedding_natCast, range_natCast ▸ isOpen_Iio⟩

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

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

Разделы

Аффилиация

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