map_one

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.map_one

English

For any φ in a suitable FunLike/Functor class, map φ 1 = 1, i.e., sending the unit via φ yields the unit.

Русский

Для любого φ в подходящем классе FunLike/OneHom, map φ 1 = 1, то есть отправка единицы через φ сохраняет единицу.

LaTeX

$$$\\mathrm{map}(\\phi, 1) = 1$$$

Lean4

@[to_additive]
protected theorem map_one [FunLike F α β] [OneHomClass F α β] (φ : F) : map φ 1 = 1 := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru