map₂_coe — Mathlib

English

Applying map₂ to constant germs recovers the pointwise operation on functions.

Русский

Применение map₂ к константным зародышам восстанавливает по точкам операцию на функции.

LaTeX

$$$ \mathrm{Germ.map₂}(op)(\mathrm{Germ.ofFun}f)(\mathrm{Germ.ofFun}g) = \mathrm{Germ.ofFun}(x \mapsto op(f(x))(g(x))) $$$

Lean4

@[simp]
theorem map₂_coe (op : β → γ → δ) (f : α → β) (g : α → γ) : map₂ op (f : Germ l β) g = fun x => op (f x) (g x) :=
  rfl

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