coe_map — Mathlib

English

The underlying set of the image of S under f equals the image of the set S under f; that is, (S.map f : Set B) = f '' S.

Русский

Множество образа S под действием f совпадает с изображением множества S через f: (S.map f : Set B) = f '' S.

LaTeX

$$$(S.map f : Set B) = f '' S$$$

Lean4

@[simp, norm_cast]
theorem coe_map (S : StarSubalgebra R A) (f : A →⋆ₐ[R] B) : (S.map f : Set B) = f '' S :=
  rfl

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