isEmbedding_inclusion — Mathlib

English

The inclusion map of a star subalgebra is an embedding.

Русский

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

LaTeX

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

Lean4

/-- The `StarSubalgebra.inclusion` of a star subalgebra is an embedding. -/
theorem isEmbedding_inclusion {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) : IsEmbedding (inclusion h)
    where
  eq_induced := Eq.symm induced_compose
  injective := Subtype.map_injective h Function.injective_id

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