no goals
Γ : Type u_3
R : Type u_4
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
α : Type u_2
β : Type u_1
s : SummableFamily Γ R α
f : α ↪ β
a : α
b : β
h : ¬b ∈ Set.range ↑f
⊢ toFun (embDomain s f) b = 0
rw [embDomain_apply, dif_neg h]