isClosedEmbedding_inclusion — Mathlib

English

The inclusion of a closed star subalgebra is a closed embedding.

Русский

Вложение замкнутой звездной подпалгебры является замкнутым вложением.

LaTeX

$$$\mathrm{IsClosedEmbedding}(\mathrm{inclusion})$$$

Lean4

/-- The `StarSubalgebra.inclusion` of a closed star subalgebra is a `IsClosedEmbedding`. -/
theorem isClosedEmbedding_inclusion {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) (hS₁ : IsClosed (S₁ : Set A)) :
    IsClosedEmbedding (inclusion h) :=
  { IsEmbedding.inclusion h with
    isClosed_range :=
      isClosed_induced_iff.2
        ⟨S₁, hS₁, by
          convert (Set.range_subtype_map id _).symm
          · rw [Set.image_id]; rfl
          · intro _ h'
            apply h h'⟩ }

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