rangeRestrict — Mathlib

English

The range of a continuous algebra homomorphism f can be used as the codomain to obtain a restricted morphism.

Русский

Область значений непрерывного алгебро-морфизма f используется как кодобеспечение для получения ограниченного морфизма.

LaTeX

$$$\text{rangeRestrict}(f) = f\restriction_{\operatorname{range}(f)}$$$

Lean4

/-- Restrict the codomain of a continuous algebra homomorphism `f` to `f.range`. -/
@[reducible]
def rangeRestrict (f : A →A[R] B) :=
  f.codRestrict (@AlgHom.range R A B _ _ _ _ _ f) (@AlgHom.mem_range_self R A B _ _ _ _ _ f)

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