isClosedEmbedding_coe — Mathlib

English

The inclusion of an elemental algebra into A is a closed embedding.

Русский

Включение элементарной алгебры в A является замкнутым вложением.

LaTeX

$$Topology.IsClosedEmbedding ((\u2192) : elemental R x → A)$$

Lean4

/-- The coercion from an elemental algebra to the full algebra is a `IsClosedEmbedding`. -/
theorem isClosedEmbedding_coe (x : A) : Topology.IsClosedEmbedding ((↑) : elemental R x → A)
    where
  eq_induced := rfl
  injective := Subtype.coe_injective
  isClosed_range := by simpa using isClosed R x

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