feat(data/finset/locally_finite): add Ico_subset_Ico_union_Ico (#11710)

This lemma extends the result for `set`s to `finset`s.
leanprover-community · Feb 18, 2022 · 59a183a · 59a183a
1 parent e93996c
commit 59a183a
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/data/finset/locally_finite.lean b/src/data/finset/locally_finite.lean
@@ -373,6 +373,10 @@ lemma Ico_union_Ico_eq_Ico {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
   Ico a b ∪ Ico b c = Ico a c :=
 by rw [←coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, set.Ico_union_Ico_eq_Ico hab hbc]
 
+lemma Ico_subset_Ico_union_Ico {a b c : α} :
+  Ico a c ⊆ Ico a b ∪ Ico b c :=
+by { rw [←coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico], exact set.Ico_subset_Ico_union_Ico }
+
 lemma Ico_union_Ico' {a b c d : α} (hcb : c ≤ b) (had : a ≤ d) :
   Ico a b ∪ Ico c d = Ico (min a c) (max b d) :=
 by rw [←coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, set.Ico_union_Ico' hcb had]