chore(data/indicator_function): add a formula for the support of `ind…

…icator` (#6314) * rename `set.support_indicator` to `set.support_indicator_subset`; * add a new `set.support_indicator`; * add `function.support_comp_eq_preimage`.
leanprover-community · Feb 20, 2021 · d483bc2 · d483bc2
1 parent 3ab9818
commit d483bc2
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/src/data/indicator_function.lean b/src/data/indicator_function.lean
@@ -60,7 +60,10 @@ not_imp_comm.1 (λ hn, indicator_of_not_mem hn f) h
 
 lemma eq_on_indicator : eq_on (indicator s f) f s := λ x hx, indicator_of_mem hx f
 
-lemma support_indicator : function.support (s.indicator f) ⊆ s :=
+@[simp] lemma support_indicator : function.support (s.indicator f) = s ∩ function.support f :=
+ext $ λ x, by simp [function.mem_support]
+
+lemma support_indicator_subset : function.support (s.indicator f) ⊆ s :=
 λ x hx, hx.imp_symm (λ h, indicator_of_not_mem h f)
 
 @[simp] lemma indicator_apply_eq_self : s.indicator f a = f a ↔ (a ∉ s → f a = 0) :=

diff --git a/src/topology/algebra/infinite_sum.lean b/src/topology/algebra/infinite_sum.lean
@@ -104,7 +104,7 @@ subtype.coe_injective.has_sum_iff $ by simpa using support_subset_iff'.1 hf
 lemma has_sum_subtype_iff_indicator {s : set β} :
   has_sum (f ∘ coe : s → α) a ↔ has_sum (s.indicator f) a :=
 by rw [← set.indicator_range_comp, subtype.range_coe,
-  has_sum_subtype_iff_of_support_subset set.support_indicator]
+  has_sum_subtype_iff_of_support_subset set.support_indicator_subset]
 
 @[simp] lemma has_sum_subtype_support : has_sum (f ∘ coe : support f → α) a ↔ has_sum f a :=
 has_sum_subtype_iff_of_support_subset $ set.subset.refl _