isClosedEmbedding_coe — Mathlib

English

For every x ∈ A, the natural inclusion of the elemental subalgebra generated by x into A is a closed embedding.

Русский

Пусть x ∈ A. Натуральное вложение элементарной подалгебры, порожденной x, в A является замкнутым вложением.

LaTeX

$$$\iota_x:\operatorname{elemental}(R,x) \hookrightarrow A\quad\text{is a closed embedding}$$$

Lean4

/-- The coercion from an elemental algebra to the full algebra as 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

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