English
If s is a Finset and f : ι →₀ α, t : ι → Finset α, then membership in s.finsupp t is equivalent to f being pointwise in t, under the obvious support condition.
Русский
Пусть s — множество Finset, f : ι →₀ α, t : ι → Finset α. Членство f в s.finsupp t эквивалентно тому, что f(i) ∈ t(i) для всех i, при условии поддержки.
LaTeX
$$$g \\in f.s.pi \\Longleftrightarrow \\forall i,\\ g(i) \\in f(i)$$$
Lean4
/-- When `t` is supported on `s`, `f ∈ s.finsupp t` precisely means that `f` is pointwise in `t`. -/
@[simp]
theorem mem_finsupp_iff_of_support_subset {t : ι →₀ Finset α} (ht : t.support ⊆ s) : f ∈ s.finsupp t ↔ ∀ i, f i ∈ t i :=
by
refine
mem_finsupp_iff.trans
(forall_and.symm.trans <|
forall_congr' fun i =>
⟨fun h => ?_, fun h => ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi ?_, fun _ => h⟩⟩)
· by_cases hi : i ∈ s
· exact h.2 hi
· rw [notMem_support_iff.1 (mt h.1 hi), notMem_support_iff.1 fun H => hi <| ht H]
exact zero_mem_zero
· rwa [H, mem_zero] at h
