English
Let t : ι → Finset α and s ⊆ ι be finite. For f ∈ ι →₀ α, membership in the finset s.finsupp t is characterized by: f ∈ s.finsupp t if and only if the support of f is contained in s and for every i ∈ s we have f(i) ∈ t(i).
Русский
Пусть t : ι → Finset α и s ⊆ ι конечна. Для f ∈ ι →₀ α членство в Finset f.s finsupp t эквивалентно тому, что опора f ⊆ s и для каждого i ∈ s выполняется f(i) ∈ t(i).
LaTeX
$$$f \\in s.finsupp t \\;\\Longleftrightarrow\\; f_{support} \\subseteq s \\ \\land\\ \\forall i \\in s,\\ f(i) \\in t(i)$$$
Lean4
theorem mem_finsupp_iff {t : ι → Finset α} : f ∈ s.finsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i := by
classical
refine mem_map.trans ⟨?_, ?_⟩
· rintro ⟨f, hf, rfl⟩
refine ⟨support_indicator_subset _ _, fun i hi => ?_⟩
convert mem_pi.1 hf i hi
exact indicator_of_mem hi _
· refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
ext i
exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm
