map_of — Mathlib

English

For any f: α → β, the map sends the generator of x to the generator of f(x): map f (of x) = of (f x).

Русский

Для любого f: α → β отображение отправляет образ порождающего x в образ порождающего f(x): map f (of x) = of (f x).

LaTeX

$$$$\forall x:\alpha,\; \mathrm{map}(f)(\mathrm{of}(x)) = \mathrm{of}(f(x)).$$$$

Lean4

@[simp]
theorem map_of (x : α) : map f (of x) = of (f x) :=
  lift_of _ _

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