isClosedEmbedding_toContinuousMap

English

For [T1Space R], the inclusion map from C(X,R)₀ to C(X,R) is a closed embedding; i.e., its range is closed and it is an embedding.

Русский

При [T1Space R] вложение C(X,R)₀ → C(X,R) является замкнутым вложением: образ замкнут и отображение инъективно.

LaTeX

$$$[T1Space R] : IsClosedEmbedding\\bigl( \\uparrow : C(X,R)_0 \\to C(X,R) \\bigr)$$$

Lean4

theorem isClosedEmbedding_toContinuousMap [T1Space R] : IsClosedEmbedding ((↑) : C(X, R)₀ → C(X, R))
    where
  toIsEmbedding := isEmbedding_toContinuousMap
  isClosed_range := by
    rw [range_toContinuousMap]
    exact isClosed_singleton.preimage <| continuous_eval_const 0

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