inclusion — Mathlib

English

If hs expresses s = ↑S, then S.copy s hs = S.

Русский

Если hs задаёт s = ↑S, то S.copy s hs = S.

LaTeX

$$$S.copy\, s\, hs = S$ when $hs$ expresses $s = \uparrow S$$$

Lean4

/-- The inclusion map between `StarSubalgebra`s given by `Subtype.map id` as a `StarAlgHom`. -/
@[simps]
def inclusion {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) : S₁ →⋆ₐ[R] S₂
    where
  toFun := Subtype.map id h
  map_one' := rfl
  map_mul' _ _ := rfl
  map_zero' := rfl
  map_add' _ _ := rfl
  commutes' _ := rfl
  map_star' _ := rfl

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