isOpenEmbedding_coe — Mathlib

English

The inclusion i: R → EReal is an open embedding; its image is an open subspace of EReal.

Русский

Вставка i: R → EReal является открытым вложением; образ является открытым подпростразми в EReal.

LaTeX

$$$\\iota:\\mathbb{R}\\to \\mathrm{EReal},\\; \\iota(x)=x\\ \\text{ is an open embedding}$$$

Lean4

theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℝ → EReal) :=
  ⟨isEmbedding_coe, by simp only [range_coe_eq_Ioo, isOpen_Ioo]⟩

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