English
If t is supported on s (i.e., t.support ⊆ s), then f ∈ s.dfinsupp t if and only if ∀ i, f(i) ∈ t(i).
Русский
Если t поддержан на s (t.support ⊆ s), то f ∈ s.dfinsupp t тогда и только тогда, когда ∀ i, f(i) ∈ t(i).
LaTeX
$$f ∈ s.dfinsupp t ⇔ ∀ i, f(i) ∈ t(i), given t.support ⊆ s$$
Lean4
/-- When `t` is supported on `s`, `f ∈ s.dfinsupp t` precisely means that `f` is pointwise in `t`.
-/
@[simp]
theorem mem_dfinsupp_iff_of_support_subset {t : Π₀ i, Finset (α i)} (ht : t.support ⊆ s) :
f ∈ s.dfinsupp t ↔ ∀ i, f i ∈ t i :=
by
refine
mem_dfinsupp_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 (notMem_mono ht hi)]
exact zero_mem_zero
· rwa [H, mem_zero] at h
