English
An element f lies in s.dfinsupp t exactly when its support is contained in s and every coordinate i ∈ s satisfies f(i) ∈ t(i).
Русский
Элемент f принадлежит s.dfinsupp t тогда и только тогда, когда поддержка f ⊆ s и для каждого i ∈ s выполняется f(i) ∈ t(i).
LaTeX
$$f ∈ s.dfinsupp t ⇔ f.\mathrm{support} ⊆ s ∧ ∀ i ∈ s, f(i) ∈ t(i)$$
Lean4
theorem mem_dfinsupp_iff : f ∈ s.dfinsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i :=
by
refine mem_map.trans ⟨?_, ?_⟩
· rintro ⟨f, hf, rfl⟩
rw [Function.Embedding.coeFn_mk]
refine ⟨support_mk_subset, fun i hi => ?_⟩
convert mem_pi.1 hf i hi
exact mk_of_mem hi
· refine fun h => ⟨fun i _ => f i, mem_pi.2 h.2, ?_⟩
ext i
dsimp
exact ite_eq_left_iff.2 fun hi => (notMem_support_iff.1 fun H => hi <| h.1 H).symm
