feat(analysis/asymptotics/asymptotics): add is_O.exists_mem_basis (#…

…13973)
leanprover-community · May 6, 2022 · 97c4d4e · 97c4d4e
1 parent d989305
commit 97c4d4e
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/analysis/asymptotics/asymptotics.lean b/src/analysis/asymptotics/asymptotics.lean
@@ -177,6 +177,12 @@ is_O_iff_is_O_with.trans
 lemma is_O_iff_eventually : is_O f g' l ↔ ∀ᶠ c in at_top, ∀ᶠ x in l, ∥f x∥ ≤ c * ∥g' x∥ :=
 is_O_iff_eventually_is_O_with.trans $ by simp only [is_O_with]
 
+lemma is_O.exists_mem_basis {ι} {p : ι → Prop} {s : ι → set α} (h : is_O f g' l)
+  (hb : l.has_basis p s) :
+  ∃ (c : ℝ) (hc : 0 < c) (i : ι) (hi : p i), ∀ x ∈ s i, ∥f x∥ ≤ c * ∥g' x∥ :=
+flip Exists₂.imp h.exists_pos $ λ c hc h,
+  by simpa only [is_O_with_iff, hb.eventually_iff, exists_prop] using h
+
 /-! ### Subsingleton -/
 
 @[nontriviality] lemma is_o_of_subsingleton [subsingleton E'] : is_o f' g' l :=