map — Mathlib

English

If f is a star-preserving map and r is star-normal, then f r is star-normal.

Русский

Если f — отображение, сохраняющее операцию звезды, и r звёздно-нормален, то f(r) звёздно-нормален.

LaTeX

$$$\forall f\,\forall r,\; IsStarNormal(r) \Rightarrow IsStarNormal(f(r))$$$

Lean4

protected instance map {F R S : Type*} [Mul R] [Star R] [Mul S] [Star S] [FunLike F R S] [MulHomClass F R S]
    [StarHomClass F R S] (f : F) (r : R) [hr : IsStarNormal r] : IsStarNormal (f r) where
  star_comm_self := by simpa [map_star] using congr(f $(hr.star_comm_self))

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