α : Type u_1
β : Type u_2
γ : Type ?u.341408
δ : Type ?u.341411
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
⊢ Set.indicator {b} f b = f b

α : Type u_1
β : Type u_2
γ : Type ?u.341408
δ : Type ?u.341411
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
⊢ ∀ (b' : β), b' ≠ b → Set.indicator {b} f b' = 0
α : Type u_1
β : Type u_2
γ : Type ?u.341408
δ : Type ?u.341411
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
⊢ (∑' (x : ↑{b}), f ↑x) = f b
rw [_root_.tsum_subtype, tsum_eq_single b]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.341408
δ : Type ?u.341411
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
⊢ Set.indicator {b} f b = f b
simp
α : Type u_1
β : Type u_2
γ : Type ?u.341408
δ : Type ?u.341411
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
b' : β
hb' : b' ≠ b
⊢ Set.indicator {b} f b' = 0
α : Type u_1
β : Type u_2
γ : Type ?u.341408
δ : Type ?u.341411
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
⊢ ∀ (b' : β), b' ≠ b → Set.indicator {b} f b' = 0
intro b' hb'
case h
α : Type u_1
β : Type u_2
γ : Type ?u.341408
δ : Type ?u.341411
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
b' : β
hb' : b' ≠ b
⊢ ¬b' ∈ {b}
α : Type u_1
β : Type u_2
γ : Type ?u.341408
δ : Type ?u.341411
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
b' : β
hb' : b' ≠ b
⊢ Set.indicator {b} f b' = 0
rw [Set.indicator_of_not_mem]
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.341408
δ : Type ?u.341411
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f✝ g : β → α
a a₁ a₂ : α
b : β
f : β → α
b' : β
hb' : b' ≠ b
⊢ ¬b' ∈ {b}
rwa [Set.mem_singleton_iff]