map'_coe

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.map'_coe

← MathLib Explorer

English

map' commutes with the coercion: applying map' to an ofFun f yields F f.

Русский

map' корректно взаимодействует с внедрением: применение map' к ofFun f даёт F f.

LaTeX

$$$ map' F hF (\mathrm{Germ.ofFun}(f)) = F(f) $$$

Lean4

@[simp]
theorem map'_coe {lc : Filter γ} (F : (α → β) → γ → δ) (hF : (l.EventuallyEq ⇒ lc.EventuallyEq) F F) (f : α → β) :
    map' F hF f = F f :=
  rfl

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

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

Разделы

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

Аффилиация

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