toNonUnitalSubsemiring' — Mathlib

English

The forgetful map from NonUnitalSubalgebra to NonUnitalSubsemiring is an order-embedding.

Русский

Отображение от NonUnitalSubalgebra к NonUnitalSubsemiring является вложением по порядку.

LaTeX

$$def toNonUnitalSubsemiring' : NonUnitalSubalgebra(R,A) ↪o NonUnitalSubsemiring A$$

Lean4

/-- The forgetful map from `NonUnitalSubalgebra` to `NonUnitalSubsemiring` as an
`OrderEmbedding` -/
def toNonUnitalSubsemiring' [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] :
    NonUnitalSubalgebra R A ↪o NonUnitalSubsemiring A
    where
  toEmbedding :=
    { toFun := fun S => S.toNonUnitalSubsemiring
      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

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