map_mem — Mathlib

English

Under suitable assumptions, there is SMulCommClass between unitary subtypes, ensuring compatible scalar actions.

Русский

При соответствующих условиях существует SMulCommClass между подтипами унитарных элементов, обеспечивающий совместимость действий скаляров.

LaTeX

$$$\\text{SMulCommClass}(\\mathrm{unitary}(R), \\mathrm{unitary}(S), \\mathrm{unitary}(A))$$$

Lean4

theorem map_mem {F : Type*} [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) {r : R}
    (hr : r ∈ unitary R) : f r ∈ unitary S := by
  rw [unitary.mem_iff] at hr
  simpa [map_star, map_mul] using And.intro congr(f $(hr.1)) congr(f $(hr.2))

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