option_map

Mathlib.Logic.Function.Conjugate

URI: https://scilib.ai/kg/mathlib#Function.Commute.option_map

← MathLib Explorer

English

If f commutes with g, then Option.map f commutes with Option.map g.

Русский

Если f коммутирует с g, то Option.map f коммутирует с Option.map g.

LaTeX

$$$ \text{Commute } (Option.map f) (Option.map g) $$$

Lean4

/-- If `f` commutes with `g`, then `Option.map f` commutes with `Option.map g`. -/
nonrec theorem option_map {f g : α → α} (h : Commute f g) : Commute (Option.map f) (Option.map g) :=
  h.option_map

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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