English
If f has finite μ-measurable support and g has finite μ-measurable support, then the mapped pair (f.map(uncurry op)) has finite μ-measurable support for any binary operation op with zero-result condition.
Русский
Если f и g имеют конечную μ-опору, то отображение через операцию двух аргументов образует конечную μ-опору на пару.
LaTeX
$$$\forall f,g,\; \mathrm{FinMeasSupp}(f,\mu) \land \mathrm{FinMeasSupp}(g,\mu) \Rightarrow \mathrm{FinMeasSupp}(\mathrm{map}(\mathrm{uncurry\,op})(\mathrm{pair}(f,g)),\mu) \quad (\text{при } op\,0\,0=0)$$$
Lean4
protected theorem pair {g : α →ₛ γ} (hf : f.FinMeasSupp μ) (hg : g.FinMeasSupp μ) : (pair f g).FinMeasSupp μ :=
calc
μ (support <| pair f g) = μ (support f ∪ support g) := congr_arg μ <| support_prodMk f g
_ ≤ μ (support f) + μ (support g) := (measure_union_le _ _)
_ < _ := add_lt_top.2 ⟨hf, hg⟩
