rangeIcc — Mathlib

English

For any f,g, (rangeIcc f g)(i) = Icc(f(i), g(i)).

Русский

Для любых f,g верно: (rangeIcc f g)(i) = Icc(f(i), g(i)).

LaTeX

$$$ (rangeIcc\\; f\\; g)(i) = Icc(f(i), g(i)) $$$

Lean4

/-- Pointwise `Finset.Icc` bundled as a `Finsupp`. -/
@[simps toFun]
def rangeIcc (f g : ι →₀ α) : ι →₀ Finset α
    where
  toFun i := Icc (f i) (g i)
  support := f.support ∪ g.support
  mem_support_toFun
    i := by
    rw [mem_union, ← not_iff_not, not_or, notMem_support_iff, notMem_support_iff, not_ne_iff]
    exact Icc_eq_singleton_iff.symm

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