valA — Mathlib

English

The subalgebra-valued map p ↦ p.valA is the natural inclusion from p into A, i.e., it records the inclusion as a continuous algebra homomorphism.

Русский

Отображение p ↦ p.valA есть естественное включение из p в A, то есть запись включения как непрерывного алгебро-гомоморфизма.

LaTeX

$$$p\mapsto p.{\text{valA}} = p.{\text{subtype}}$$$

Lean4

/-- `Subalgebra.val` as a `ContinuousAlgHom`. -/
def _root_.Subalgebra.valA (p : Subalgebra R A) : p →A[R] A
    where
  cont := continuous_subtype_val
  toAlgHom := p.val

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