From 59a183a18829a4e4774ebb6c927297101acad19e Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Fri, 18 Feb 2022 00:52:54 +0000 Subject: [PATCH] feat(data/finset/locally_finite): add Ico_subset_Ico_union_Ico (#11710) This lemma extends the result for `set`s to `finset`s. --- src/data/finset/locally_finite.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/data/finset/locally_finite.lean b/src/data/finset/locally_finite.lean index 82c7a04335350..d27ce710a0f4b 100644 --- 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]