map' — Mathlib

English

A construction map' lifts a function on functions to a map between germs with a compatibility condition.

Русский

Конструкция map' поднимает отображение функций до отображения между зародышами при наличии совместимости.

LaTeX

$$$ \mathrm{map'}_{lc}(F, hF) : \mathrm{Germ}(l, \beta) \to \mathrm{Germ}(lc, \delta)$$$

Lean4

/-- Given a map `F : (α → β) → (γ → δ)` that sends functions eventually equal at `l` to functions
eventually equal at `lc`, returns a map from `Germ l β` to `Germ lc δ`. -/
def map' {lc : Filter γ} (F : (α → β) → γ → δ) (hF : (l.EventuallyEq ⇒ lc.EventuallyEq) F F) : Germ l β → Germ lc δ :=
  Quotient.map' F hF

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