toNonUnitalSubalgebra' — Mathlib

English

There is an order-embedding from NonUnitalStarSubalgebra to NonUnitalSubalgebra sending S to its underlying subalgebra.

Русский

Существует вложение порядка от NonUnitalStarSubalgebra в NonUnitalSubalgebra, отправляющее S в его базовую подплощадку.

LaTeX

$$toNonUnitalSubalgebra' : NonUnitalStarSubalgebra R A \hookrightarrow^{{\mathrm{order}}} NonUnitalSubalgebra R A$$

Lean4

/-- The forgetful map from `NonUnitalStarSubalgebra` to `NonUnitalSubalgebra` as an
`OrderEmbedding` -/
def toNonUnitalSubalgebra' : NonUnitalStarSubalgebra R A ↪o NonUnitalSubalgebra R A
    where
  toEmbedding :=
    { toFun := fun S => S.toNonUnitalSubalgebra
      inj' := fun S T h => ext <| by apply SetLike.ext_iff.1 h }
  map_rel_iff' := SetLike.coe_subset_coe.symm.trans SetLike.coe_subset_coe

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