isEmbedding_coe — Mathlib

English

Let EReal be the extended real numbers. The natural inclusion i: R → EReal, i(x) = x, is a topological embedding; in particular it is injective and induces the subspace topology on its image.

Русский

Пусть EReal – это дополненные вещественные числа. Встроение i: R → EReal, i(x) = x, является топологическим вложением; например, оно инъективно и топология на образе совпадает с подпространственной топологией.

LaTeX

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

Lean4

theorem isEmbedding_coe : IsEmbedding ((↑) : ℝ → EReal) :=
  coe_strictMono.isEmbedding_of_ordConnected <| by rw [range_coe_eq_Ioo]; exact ordConnected_Ioo

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