map_one' — Mathlib

English

For any function f : α → β, map f on the unit filter equals the principal of f(1): map f 1 = pure (f 1).

Русский

Для любой функции f: α → β отображение единичного фильтра через f равно чистому фильтру f(1): map f 1 = pure (f 1).

LaTeX

$$$\\mathrm{map}(f, 1) = \\mathrm{pure}(f(1))$$$

Lean4

@[to_additive (attr := simp)]
protected theorem map_one' (f : α → β) : (1 : Filter α).map f = pure (f 1) :=
  rfl

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