feat(data/indicator_function): eq_self_of_superset (#6829)

leanprover-community · Mar 23, 2021 · ee5e9fb · ee5e9fb
1 parent aadd853
commit ee5e9fb
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/data/indicator_function.lean b/src/data/indicator_function.lean
@@ -73,6 +73,9 @@ ite_eq_left_iff.trans $ by rw [@eq_comm _ (f a)]
 @[simp] lemma indicator_eq_self : s.indicator f = f ↔ support f ⊆ s :=
 by simp only [funext_iff, subset_def, mem_support, indicator_apply_eq_self, not_imp_comm]
 
+lemma indicator_eq_self_of_superset (h1 : s.indicator f = f) (h2 : s ⊆ t) : t.indicator f = f :=
+by { rw indicator_eq_self at h1 ⊢, exact subset.trans h1 h2 }
+
 @[simp] lemma indicator_support : (support f).indicator f = f :=
 indicator_eq_self.2 $ subset.refl _