codRestrict — Mathlib

English

Same as ext_of_adjoin_eq_top for adjoin equaling top with another hs.

Русский

Та же формулировка ext_of_adjoin_eq_top с другим набором hs.

LaTeX

$$$ (\\mathrm{adjoin}_R s = \\top) \\Rightarrow (\\forall x, x \\in s \\Rightarrow \\dots)$$$

Lean4

/-- Restriction of the codomain of a `StarAlgHom` to a star subalgebra containing the range. -/
protected def codRestrict (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ x, f x ∈ S) : A →⋆ₐ[R] S
    where
  toAlgHom := AlgHom.codRestrict f.toAlgHom S.toSubalgebra hf
  map_star' := fun x => Subtype.ext (map_star f x)

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