isClosedEmbedding_coe — Mathlib

English

The natural inclusion map from elemental R x to A is a closed embedding.

Русский

Естественное вложение элементарного R x в A является замкнутым вложением.

LaTeX

$$IsClosedEmbedding ((↑) : elemental R x → A)$$

Lean4

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

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