map₂ — Mathlib

English

Lift a binary function to germs to obtain a germ-valued function of two germ arguments.

Русский

Поднять бинарную функцию до зародышей, получая функцию из двух зародышей в зародыш.

LaTeX

$$$ \mathrm{map₂}(op) : \mathrm{Germ}(l, \beta) \to \mathrm{Germ}(l, \gamma) \to \mathrm{Germ}(l, \delta)$$$

Lean4

/-- Lift a binary function `β → γ → δ` to a function `Germ l β → Germ l γ → Germ l δ`. -/
def map₂ (op : β → γ → δ) : Germ l β → Germ l γ → Germ l δ :=
  Quotient.map₂ (fun f g x => op (f x) (g x)) fun f f' Hf g g' Hg =>
    Hg.mp <| Hf.mono fun x Hf Hg => by simp only [Hf, Hg]

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