coe_map — Mathlib

English

Let f be a map from R to S and s be a subsemiring of R. Then the carrier of the image s.map f equals the image of the carrier s under f; that is, the set of elements of S obtainable by applying f to elements of s.

Русский

Пусть f: R → S, и s — подполусемиринг в R. Тогда множество s.map f состоит из всех значений f(x) с x∈s; то есть carrier совпадает с образами элементов s под действием f.

LaTeX

$$$ (s.map f : Set S) = \{ f(x) \mid x \in s \} $$$

Lean4

@[simp]
theorem coe_map (f : F) (s : NonUnitalSubsemiring R) : (s.map f : Set S) = f '' s :=
  rfl

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