English
Let f: ℕ ∪ {∞} → ℝ be defined by f(n) = 1/(n+1) for n ∈ ℕ and f(∞) = 0. Then f is a closed embedding.
Русский
Пусть f: ℕ ∪ {∞} → ℝ задана как f(n) = 1/(n+1) при n ∈ ℕ и f(∞) = 0. Тогда f является замкнутым вложением.
LaTeX
$$$IsClosedEmbedding(natUnionInftyEmbedding)$$$
Lean4
/-- The continuous map from `ℕ∪{∞}` to `ℝ` sending `n` to `1/(n+1)` and `∞` to `0` is a closed
embedding.
-/
theorem isClosedEmbedding_natUnionInftyEmbedding : IsClosedEmbedding natUnionInftyEmbedding :=
by
refine .of_continuous_injective_isClosedMap natUnionInftyEmbedding.continuous ?_ ?_
· rintro (_ | n) (_ | m) h
· rfl
· simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, zero_eq_inv] at h
assumption_mod_cast
· simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_eq_zero] at h
assumption_mod_cast
· simp only [natUnionInftyEmbedding, one_div, ContinuousMap.coe_mk, inv_inj, add_left_inj, Nat.cast_inj] at h
rw [h]
· exact fun _ hC => (hC.isCompact.image natUnionInftyEmbedding.continuous).isClosed
