map₂ — Mathlib

English

If f and g have finite μ-measurable support, then the mapped function (f.pair g).map (uncurry op) has finite μ-measurable support whenever op 0 0 = 0.

Русский

Если f и g имеют конечную μ-опору, то отображение через пару и последующее отображение операцией имеет конечную μ-опору при условии op 0 0 = 0.

LaTeX

$$$\mathrm{FinMeasSupp}(f,\mu) \to \mathrm{FinMeasSupp}(g,\mu) \to (\mathrm{pair}(f,g)).map(\mathrm{uncurry\,op}) \;\mathrm{ FinMeasSupp }\mu$ при $op(0,0)=0$$$

Lean4

protected theorem map₂ [Zero δ] (hf : f.FinMeasSupp μ) {g : α →ₛ γ} (hg : g.FinMeasSupp μ) {op : β → γ → δ}
    (H : op 0 0 = 0) : ((pair f g).map (Function.uncurry op)).FinMeasSupp μ :=
  (hf.pair hg).map H

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