rangeSingleton — Mathlib

English

rangeSingleton maps a finsupp f to a finsupp of Finset α, with (rangeSingleton f)(i) = {f(i)}.

Русский

rangeSingleton переводит finsupp f в finsupp, где at i лежит множество {f(i)}.

LaTeX

$$$ (\\mathrm{rangeSingleton} f)(i) = \\{ f(i) \\} $$$

Lean4

/-- Pointwise `Singleton.singleton` bundled as a `Finsupp`. -/
@[simps]
def rangeSingleton (f : ι →₀ α) : ι →₀ Finset α where
  toFun i := {f i}
  support := f.support
  mem_support_toFun
    i := by
    rw [← not_iff_not, notMem_support_iff, not_ne_iff]
    exact singleton_injective.eq_iff.symm

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