English
The rangeIcc construction gives, pointwise, Finsets Icc(f(i), g(i)) for each i, collected into a DFinsupp.
Русский
Конструкция rangeIcc задаёт по каждой i Finset Icc(f(i), g(i)) и собирает их в DFinsupp.
LaTeX
$$rangeIcc (f g) : DFinsupp fun i => Finset (α i) with toFun i := Icc (f i) (g i)$$
Lean4
/-- Pointwise `Finset.Icc` bundled as a `DFinsupp`. -/
def rangeIcc (f g : Π₀ i, α i) : Π₀ i, Finset (α i)
where
toFun i := Icc (f i) (g i)
support' :=
f.support'.bind fun fs =>
g.support'.map fun gs =>
⟨fs.1 + gs.1, fun i =>
or_iff_not_imp_left.2 fun h =>
by
have hf : f i = 0 :=
(fs.prop i).resolve_left (Multiset.notMem_mono (Multiset.Le.subset <| Multiset.le_add_right _ _) h)
have hg : g i = 0 :=
(gs.prop i).resolve_left (Multiset.notMem_mono (Multiset.Le.subset <| Multiset.le_add_left _ _) h)
simp_rw [hf, hg]
exact Icc_self _⟩
