map₂_const — Mathlib

English

Applying a binary operation f to two constant germs yields the constant germ of f(b,c).

Русский

При двоичной операции f к двум константным жермам получается константная жерма значения f(b,c).

LaTeX

$$$ \\mathrm{map₂} f (\\uparrow b : \\mathrm{Germ}(l,\\beta)) (\\uparrow c : \\mathrm{Germ}(l,\\gamma)) = \\uparrow (f\\, b\\, c) $$$

Lean4

@[simp]
theorem map₂_const (l : Filter α) (b : β) (c : γ) (f : β → γ → δ) : map₂ f (↑b : Germ l β) ↑c = ↑(f b c) :=
  rfl

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