refactor(*): migrate from filter.lift' _ powerset to filter.small_sets (#13673)

Author: urkud

src/analysis/special_functions/non_integrable.lean

@@ -60,7 +60,7 @@ begin
   { rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩,
     have h : ∀ᶠ x : ℝ × ℝ in l.prod l, ∀ y ∈ [x.1, x.2], (differentiable_at ℝ f y ∧
       ∥deriv f y∥ ≤ C * ∥g y∥) ∧ y ∈ [a, b],
-      from (tendsto_fst.interval tendsto_snd).eventually ((hd.and hC.bound).and hl).lift'_powerset,
+      from (tendsto_fst.interval tendsto_snd).eventually ((hd.and hC.bound).and hl).small_sets,
     rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩,
     simp only [prod_subset_iff, mem_set_of_eq] at hs,
     exact ⟨C, C₀, s, hsl, λ x hx y hy z hz, (hs x hx y hy z hz).2,

src/measure_theory/integral/integrable_on.lean

@@ -38,8 +38,8 @@ def strongly_measurable_at_filter (f : α → β) (l : filter α) (μ : measure
 ⟨∅, mem_bot, by simp⟩
 
 protected lemma strongly_measurable_at_filter.eventually (h : strongly_measurable_at_filter f l μ) :
-  ∀ᶠ s in l.lift' powerset, ae_strongly_measurable f (μ.restrict s) :=
-(eventually_lift'_powerset' $ λ s t, ae_strongly_measurable.mono_set).2 h
+  ∀ᶠ s in l.small_sets, ae_strongly_measurable f (μ.restrict s) :=
+(eventually_small_sets' $ λ s t, ae_strongly_measurable.mono_set).2 h
 
 protected lemma strongly_measurable_at_filter.filter_mono
   (h : strongly_measurable_at_filter f l μ) (h' : l' ≤ l) :
@@ -246,15 +246,15 @@ begin
 end
 
 /-- We say that a function `f` is *integrable at filter* `l` if it is integrable on some
-set `s ∈ l`. Equivalently, it is eventually integrable on `s` in `l.lift' powerset`. -/
+set `s ∈ l`. Equivalently, it is eventually integrable on `s` in `l.small_sets`. -/
 def integrable_at_filter (f : α → E) (l : filter α) (μ : measure α . volume_tac) :=
 ∃ s ∈ l, integrable_on f s μ
 
 variables {l l' : filter α}
 
 protected lemma integrable_at_filter.eventually (h : integrable_at_filter f l μ) :
-  ∀ᶠ s in l.lift' powerset, integrable_on f s μ :=
-by { refine (eventually_lift'_powerset' $ λ s t hst ht, _).2 h, exact ht.mono_set hst }
+  ∀ᶠ s in l.small_sets, integrable_on f s μ :=
+iff.mpr (eventually_small_sets' $ λ s t hst ht, ht.mono_set hst) h
 
 lemma integrable_at_filter.filter_mono (hl : l ≤ l') (hl' : integrable_at_filter f l' μ) :
   integrable_at_filter f l μ :=
@@ -289,9 +289,9 @@ lemma measure.finite_at_filter.integrable_at_filter {l : filter α} [is_measurab
   (hf : l.is_bounded_under (≤) (norm ∘ f)) :
   integrable_at_filter f l μ :=
 begin
-  obtain ⟨C, hC⟩ : ∃ C, ∀ᶠ s in (l.lift' powerset), ∀ x ∈ s, ∥f x∥ ≤ C,
-    from hf.imp (λ C hC, eventually_lift'_powerset.2 ⟨_, hC, λ t, id⟩),
-  rcases (hfm.eventually.and (hμ.eventually.and hC)).exists_measurable_mem_of_lift'
+  obtain ⟨C, hC⟩ : ∃ C, ∀ᶠ s in l.small_sets, ∀ x ∈ s, ∥f x∥ ≤ C,
+    from hf.imp (λ C hC, eventually_small_sets.2 ⟨_, hC, λ t, id⟩),
+  rcases (hfm.eventually.and (hμ.eventually.and hC)).exists_measurable_mem_of_small_sets
     with ⟨s, hsl, hsm, hfm, hμ, hC⟩,
   refine ⟨s, hsl, ⟨hfm, has_finite_integral_restrict_of_bounded hμ _⟩⟩,
   exact C,

src/measure_theory/integral/set_integral.lean

@@ -30,7 +30,7 @@ Finally, we prove a version of the
 for set integral, see `filter.tendsto.integral_sub_linear_is_o_ae` and its corollaries.
 Namely, consider a measurably generated filter `l`, a measure `μ` finite at this filter, and
 a function `f` that has a finite limit `c` at `l ⊓ μ.ae`. Then `∫ x in s, f x ∂μ = μ s • c + o(μ s)`
-as `s` tends to `l.lift' powerset`, i.e. for any `ε>0` there exists `t ∈ l` such that
+as `s` tends to `l.small_sets`, i.e. for any `ε>0` there exists `t ∈ l` such that
 `∥∫ x in s, f x ∂μ - μ s • c∥ ≤ ε * μ s` whenever `s ⊆ t`. We also formulate a version of this
 theorem for a locally finite measure `μ` and a function `f` continuous at a point `a`.
 
@@ -600,9 +600,8 @@ variables {ι : Type*} [normed_group E]
 
 /-- Fundamental theorem of calculus for set integrals: if `μ` is a measure that is finite at a
 filter `l` and `f` is a measurable function that has a finite limit `b` at `l ⊓ μ.ae`, then `∫ x in
-s i, f x ∂μ = μ (s i) • b + o(μ (s i))` at a filter `li` provided that `s i` tends to `l.lift'
-powerset` along `li`. Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).to_real` in the
-actual statement.
+s i, f x ∂μ = μ (s i) • b + o(μ (s i))` at a filter `li` provided that `s i` tends to `l.small_sets`
+along `li`. Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).to_real` in the actual statement.
 
 Often there is a good formula for `(μ (s i)).to_real`, so the formalization can take an optional
 argument `m` with this formula and a proof `of `(λ i, (μ (s i)).to_real) =ᶠ[li] m`. Without these
@@ -612,17 +611,16 @@ lemma filter.tendsto.integral_sub_linear_is_o_ae
   {μ : measure α} {l : filter α} [l.is_measurably_generated]
   {f : α → E} {b : E} (h : tendsto f (l ⊓ μ.ae) (𝓝 b))
   (hfm : strongly_measurable_at_filter f l μ) (hμ : μ.finite_at_filter l)
-  {s : ι → set α} {li : filter ι} (hs : tendsto s li (l.lift' powerset))
+  {s : ι → set α} {li : filter ι} (hs : tendsto s li l.small_sets)
   (m : ι → ℝ := λ i, (μ (s i)).to_real)
   (hsμ : (λ i, (μ (s i)).to_real) =ᶠ[li] m . tactic.interactive.refl) :
   is_o (λ i, ∫ x in s i, f x ∂μ - m i • b) m li :=
 begin
-  suffices : is_o (λ s, ∫ x in s, f x ∂μ - (μ s).to_real • b) (λ s, (μ s).to_real)
-    (l.lift' powerset),
+  suffices : is_o (λ s, ∫ x in s, f x ∂μ - (μ s).to_real • b) (λ s, (μ s).to_real) l.small_sets,
     from (this.comp_tendsto hs).congr' (hsμ.mono $ λ a ha, ha ▸ rfl) hsμ,
   refine is_o_iff.2 (λ ε ε₀, _),
-  have : ∀ᶠ s in l.lift' powerset, ∀ᶠ x in μ.ae, x ∈ s → f x ∈ closed_ball b ε :=
-    eventually_lift'_powerset_eventually.2 (h.eventually $ closed_ball_mem_nhds _ ε₀),
+  have : ∀ᶠ s in l.small_sets, ∀ᶠ x in μ.ae, x ∈ s → f x ∈ closed_ball b ε :=
+    eventually_small_sets_eventually.2 (h.eventually $ closed_ball_mem_nhds _ ε₀),
   filter_upwards [hμ.eventually, (hμ.integrable_at_filter_of_tendsto_ae hfm h).eventually,
     hfm.eventually, this],
   simp only [mem_closed_ball, dist_eq_norm],
@@ -635,7 +633,7 @@ end
 /-- Fundamental theorem of calculus for set integrals, `nhds_within` version: if `μ` is a locally
 finite measure and `f` is an almost everywhere measurable function that is continuous at a point `a`
 within a measurable set `t`, then `∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))` at a filter `li`
-provided that `s i` tends to `(𝓝[t] a).lift' powerset` along `li`.  Since `μ (s i)` is an `ℝ≥0∞`
+provided that `s i` tends to `(𝓝[t] a).small_sets` along `li`.  Since `μ (s i)` is an `ℝ≥0∞`
 number, we use `(μ (s i)).to_real` in the actual statement.
 
 Often there is a good formula for `(μ (s i)).to_real`, so the formalization can take an optional
@@ -647,7 +645,7 @@ lemma continuous_within_at.integral_sub_linear_is_o_ae
   {μ : measure α} [is_locally_finite_measure μ] {a : α} {t : set α}
   {f : α → E} (ha : continuous_within_at f t a) (ht : measurable_set t)
   (hfm : strongly_measurable_at_filter f (𝓝[t] a) μ)
-  {s : ι → set α} {li : filter ι} (hs : tendsto s li ((𝓝[t] a).lift' powerset))
+  {s : ι → set α} {li : filter ι} (hs : tendsto s li (𝓝[t] a).small_sets)
   (m : ι → ℝ := λ i, (μ (s i)).to_real)
   (hsμ : (λ i, (μ (s i)).to_real) =ᶠ[li] m . tactic.interactive.refl) :
   is_o (λ i, ∫ x in s i, f x ∂μ - m i • f a) m li :=
@@ -657,9 +655,9 @@ exact (ha.mono_left inf_le_left).integral_sub_linear_is_o_ae
 
 /-- Fundamental theorem of calculus for set integrals, `nhds` version: if `μ` is a locally finite
 measure and `f` is an almost everywhere measurable function that is continuous at a point `a`, then
-`∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))` at `li` provided that `s` tends to `(𝓝 a).lift'
-powerset` along `li.  Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).to_real` in the
-actual statement.
+`∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))` at `li` provided that `s` tends to
+`(𝓝 a).small_sets` along `li.  Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).to_real` in
+the actual statement.
 
 Often there is a good formula for `(μ (s i)).to_real`, so the formalization can take an optional
 argument `m` with this formula and a proof `of `(λ i, (μ (s i)).to_real) =ᶠ[li] m`. Without these
@@ -669,16 +667,16 @@ lemma continuous_at.integral_sub_linear_is_o_ae
   [normed_space ℝ E] [complete_space E]
   {μ : measure α} [is_locally_finite_measure μ] {a : α}
   {f : α → E} (ha : continuous_at f a) (hfm : strongly_measurable_at_filter f (𝓝 a) μ)
-  {s : ι → set α} {li : filter ι} (hs : tendsto s li ((𝓝 a).lift' powerset))
+  {s : ι → set α} {li : filter ι} (hs : tendsto s li (𝓝 a).small_sets)
   (m : ι → ℝ := λ i, (μ (s i)).to_real)
   (hsμ : (λ i, (μ (s i)).to_real) =ᶠ[li] m . tactic.interactive.refl) :
   is_o (λ i, ∫ x in s i, f x ∂μ - m i • f a) m li :=
 (ha.mono_left inf_le_left).integral_sub_linear_is_o_ae hfm (μ.finite_at_nhds a) hs m hsμ
 
 /-- Fundamental theorem of calculus for set integrals, `nhds_within` version: if `μ` is a locally
 finite measure, `f` is continuous on a measurable set `t`, and `a ∈ t`, then `∫ x in (s i), f x ∂μ =
-μ (s i) • f a + o(μ (s i))` at `li` provided that `s i` tends to `(𝓝[t] a).lift' powerset` along
-`li`.  Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).to_real` in the actual statement.
+μ (s i) • f a + o(μ (s i))` at `li` provided that `s i` tends to `(𝓝[t] a).small_sets` along `li`.
+Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).to_real` in the actual statement.
 
 Often there is a good formula for `(μ (s i)).to_real`, so the formalization can take an optional
 argument `m` with this formula and a proof `of `(λ i, (μ (s i)).to_real) =ᶠ[li] m`. Without these
@@ -688,7 +686,7 @@ lemma continuous_on.integral_sub_linear_is_o_ae
   [normed_space ℝ E] [complete_space E] [second_countable_topology_either α E]
   {μ : measure α} [is_locally_finite_measure μ] {a : α} {t : set α}
   {f : α → E} (hft : continuous_on f t) (ha : a ∈ t) (ht : measurable_set t)
-  {s : ι → set α} {li : filter ι} (hs : tendsto s li ((𝓝[t] a).lift' powerset))
+  {s : ι → set α} {li : filter ι} (hs : tendsto s li (𝓝[t] a).small_sets)
   (m : ι → ℝ := λ i, (μ (s i)).to_real)
   (hsμ : (λ i, (μ (s i)).to_real) =ᶠ[li] m . tactic.interactive.refl) :
   is_o (λ i, ∫ x in s i, f x ∂μ - m i • f a) m li :=

src/measure_theory/measurable_space.lean

@@ -1325,10 +1325,10 @@ lemma eventually.exists_measurable_mem {f : filter α} [is_measurably_generated
   ∃ s ∈ f, measurable_set s ∧ ∀ x ∈ s, p x :=
 is_measurably_generated.exists_measurable_subset h
 
-lemma eventually.exists_measurable_mem_of_lift' {f : filter α} [is_measurably_generated f]
-  {p : set α → Prop} (h : ∀ᶠ s in f.lift' powerset, p s) :
+lemma eventually.exists_measurable_mem_of_small_sets {f : filter α} [is_measurably_generated f]
+  {p : set α → Prop} (h : ∀ᶠ s in f.small_sets, p s) :
   ∃ s ∈ f, measurable_set s ∧ p s :=
-let ⟨s, hsf, hs⟩ := eventually_lift'_powerset.1 h,
+let ⟨s, hsf, hs⟩ := eventually_small_sets.1 h,
   ⟨t, htf, htm, hts⟩ := is_measurably_generated.exists_measurable_subset hsf
 in ⟨t, htf, htm, hs t hts⟩
 

src/measure_theory/measure/measure_space.lean

@@ -2357,7 +2357,7 @@ by { filter_upwards [hs_zero], intros, split_ifs, refl }
 namespace measure
 
 /-- A measure is called finite at filter `f` if it is finite at some set `s ∈ f`.
-Equivalently, it is eventually finite at `s` in `f.lift' powerset`. -/
+Equivalently, it is eventually finite at `s` in `f.small_sets`. -/
 def finite_at_filter {m0 : measurable_space α} (μ : measure α) (f : filter α) : Prop :=
 ∃ s ∈ f, μ s < ∞
 
@@ -2908,8 +2908,8 @@ protected lemma measure_mono (h : μ ≤ ν) : ν.finite_at_filter f → μ.fini
   ν.finite_at_filter g → μ.finite_at_filter f :=
 λ h, (h.filter_mono hf).measure_mono hμ
 
-protected lemma eventually (h : μ.finite_at_filter f) : ∀ᶠ s in f.lift' powerset, μ s < ∞ :=
-(eventually_lift'_powerset' $ λ s t hst ht, (measure_mono hst).trans_lt ht).2 h
+protected lemma eventually (h : μ.finite_at_filter f) : ∀ᶠ s in f.small_sets, μ s < ∞ :=
+(eventually_small_sets' $ λ s t hst ht, (measure_mono hst).trans_lt ht).2 h
 
 lemma filter_sup : μ.finite_at_filter f → μ.finite_at_filter g → μ.finite_at_filter (f ⊔ g) :=
 λ ⟨s, hsf, hsμ⟩ ⟨t, htg, htμ⟩,

src/order/filter/interval.lean

@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
 import data.set.intervals.ord_connected
-import order.filter.lift
+import order.filter.small_sets
 import order.filter.at_top_bot
 
 /-!
 # Convergence of intervals
 
 If both `a` and `b` tend to some filter `l₁`, sometimes this implies that `Ixx a b` tends to
-`l₂.lift' powerset`, i.e., for any `s ∈ l₂` eventually `Ixx a b` becomes a subset of `s`.  Here and
+`l₂.small_sets`, i.e., for any `s ∈ l₂` eventually `Ixx a b` becomes a subset of `s`.  Here and
 below `Ixx` is one of `Icc`, `Ico`, `Ioc`, and `Ioo`. We define `filter.tendsto_Ixx_class Ixx l₁ l₂`
 to be a typeclass representing this property.
 
@@ -53,59 +53,57 @@ section preorder
 variables [preorder α]
 
 /-- A pair of filters `l₁`, `l₂` has `tendsto_Ixx_class Ixx` property if `Ixx a b` tends to
-`l₂.lift' powerset` as `a` and `b` tend to `l₁`. In all instances `Ixx` is one of `Icc`, `Ico`,
-`Ioc`, or `Ioo`. The instances provide the best `l₂` for a given `l₁`. In many cases `l₁ = l₂` but
+`l₂.small_sets` as `a` and `b` tend to `l₁`. In all instances `Ixx` is one of `Icc`, `Ico`, `Ioc`,
+or `Ioo`. The instances provide the best `l₂` for a given `l₁`. In many cases `l₁ = l₂` but
 sometimes we can drop an endpoint from an interval: e.g., we prove `tendsto_Ixx_class Ico (𝓟 $ Iic
 a) (𝓟 $ Iio a)`, i.e., if `u₁ n` and `u₂ n` belong eventually to `Iic a`, then the interval `Ico (u₁
 n) (u₂ n)` is eventually included in `Iio a`.
 
 We mark `l₂` as an `out_param` so that Lean can automatically find an appropriate `l₂` based on
 `Ixx` and `l₁`. This way, e.g., `tendsto.Ico h₁ h₂` works without specifying explicitly `l₂`. -/
 class tendsto_Ixx_class (Ixx : α → α → set α) (l₁ : filter α) (l₂ : out_param $ filter α) : Prop :=
-(tendsto_Ixx : tendsto (λ p : α × α, Ixx p.1 p.2) (l₁ ×ᶠ l₁) (l₂.lift' powerset))
+(tendsto_Ixx : tendsto (λ p : α × α, Ixx p.1 p.2) (l₁ ×ᶠ l₁) l₂.small_sets)
 
 lemma tendsto.Icc {l₁ l₂ : filter α} [tendsto_Ixx_class Icc l₁ l₂]
   {lb : filter β} {u₁ u₂ : β → α} (h₁ : tendsto u₁ lb l₁) (h₂ : tendsto u₂ lb l₁) :
-  tendsto (λ x, Icc (u₁ x) (u₂ x)) lb (l₂.lift' powerset) :=
+  tendsto (λ x, Icc (u₁ x) (u₂ x)) lb l₂.small_sets :=
 tendsto_Ixx_class.tendsto_Ixx.comp $ h₁.prod_mk h₂
 
 lemma tendsto.Ioc {l₁ l₂ : filter α} [tendsto_Ixx_class Ioc l₁ l₂]
   {lb : filter β} {u₁ u₂ : β → α} (h₁ : tendsto u₁ lb l₁) (h₂ : tendsto u₂ lb l₁) :
-  tendsto (λ x, Ioc (u₁ x) (u₂ x)) lb (l₂.lift' powerset) :=
+  tendsto (λ x, Ioc (u₁ x) (u₂ x)) lb l₂.small_sets :=
 tendsto_Ixx_class.tendsto_Ixx.comp $ h₁.prod_mk h₂
 
 lemma tendsto.Ico {l₁ l₂ : filter α} [tendsto_Ixx_class Ico l₁ l₂]
   {lb : filter β} {u₁ u₂ : β → α} (h₁ : tendsto u₁ lb l₁) (h₂ : tendsto u₂ lb l₁) :
-  tendsto (λ x, Ico (u₁ x) (u₂ x)) lb (l₂.lift' powerset) :=
+  tendsto (λ x, Ico (u₁ x) (u₂ x)) lb l₂.small_sets :=
 tendsto_Ixx_class.tendsto_Ixx.comp $ h₁.prod_mk h₂
 
 lemma tendsto.Ioo {l₁ l₂ : filter α} [tendsto_Ixx_class Ioo l₁ l₂]
   {lb : filter β} {u₁ u₂ : β → α} (h₁ : tendsto u₁ lb l₁) (h₂ : tendsto u₂ lb l₁) :
-  tendsto (λ x, Ioo (u₁ x) (u₂ x)) lb (l₂.lift' powerset) :=
+  tendsto (λ x, Ioo (u₁ x) (u₂ x)) lb l₂.small_sets :=
 tendsto_Ixx_class.tendsto_Ixx.comp $ h₁.prod_mk h₂
 
 lemma tendsto_Ixx_class_principal {s t : set α} {Ixx : α → α → set α} :
-  tendsto_Ixx_class Ixx (𝓟 s) (𝓟 t) ↔ ∀ (x ∈ s) (y ∈ s), Ixx x y ⊆ t :=
-begin
-  refine iff.trans ⟨λ h, h.1, λ h, ⟨h⟩⟩ _,
-  simp [lift'_principal monotone_powerset, -mem_prod, -prod.forall, forall_prod_set]
-end
+  tendsto_Ixx_class Ixx (𝓟 s) (𝓟 t) ↔ ∀ x y ∈ s, Ixx x y ⊆ t :=
+iff.trans ⟨λ h, h.1, λ h, ⟨h⟩⟩ $ by simp only [small_sets_principal, prod_principal_principal,
+  tendsto_principal_principal, forall_prod_set, mem_powerset_iff, mem_principal]
 
 lemma tendsto_Ixx_class_inf {l₁ l₁' l₂ l₂' : filter α} {Ixx}
   [h : tendsto_Ixx_class Ixx l₁ l₂] [h' : tendsto_Ixx_class Ixx l₁' l₂'] :
   tendsto_Ixx_class Ixx (l₁ ⊓ l₁') (l₂ ⊓ l₂') :=
-⟨by simpa only [prod_inf_prod, lift'_inf_powerset] using h.1.inf h'.1⟩
+⟨by simpa only [prod_inf_prod, small_sets_inf] using h.1.inf h'.1⟩
 
 lemma tendsto_Ixx_class_of_subset {l₁ l₂ : filter α} {Ixx Ixx' : α → α → set α}
   (h : ∀ a b, Ixx a b ⊆ Ixx' a b) [h' : tendsto_Ixx_class Ixx' l₁ l₂] :
   tendsto_Ixx_class Ixx l₁ l₂ :=
-⟨tendsto_lift'_powerset_mono h'.1 $ eventually_of_forall $ prod.forall.2 h⟩
+⟨h'.1.small_sets_mono $ eventually_of_forall $ prod.forall.2 h⟩
 
 lemma has_basis.tendsto_Ixx_class {ι : Type*} {p : ι → Prop} {s} {l : filter α}
   (hl : l.has_basis p s) {Ixx : α → α → set α}
   (H : ∀ i, p i → ∀ (x ∈ s i) (y ∈ s i), Ixx x y ⊆ s i) :
   tendsto_Ixx_class Ixx l l :=
-⟨(hl.prod_self.tendsto_iff (hl.lift' monotone_powerset)).2 $ λ i hi,
+⟨(hl.prod_self.tendsto_iff hl.small_sets).2 $ λ i hi,
   ⟨i, hi, λ x hx, H i hi _ hx.1 _ hx.2⟩⟩
 
 instance tendsto_Icc_at_top_at_top : tendsto_Ixx_class Icc (at_top : filter α) at_top :=
@@ -190,14 +188,9 @@ variable [partial_order α]
 instance tendsto_Icc_pure_pure {a : α} : tendsto_Ixx_class Icc (pure a) (pure a : filter α) :=
 by { rw ← principal_singleton, exact tendsto_Ixx_class_principal.2 ord_connected_singleton.out }
 
-instance tendsto_Ico_pure_bot {a : α} : tendsto_Ixx_class Ico (pure a) ⊥ :=
-⟨by simp [lift'_bot monotone_powerset]⟩
-
-instance tendsto_Ioc_pure_bot {a : α} : tendsto_Ixx_class Ioc (pure a) ⊥ :=
-⟨by simp [lift'_bot monotone_powerset]⟩
-
-instance tendsto_Ioo_pure_bot {a : α} : tendsto_Ixx_class Ioo (pure a) ⊥ :=
-tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Ioc_self)
+instance tendsto_Ico_pure_bot {a : α} : tendsto_Ixx_class Ico (pure a) ⊥ := ⟨by simp⟩
+instance tendsto_Ioc_pure_bot {a : α} : tendsto_Ixx_class Ioc (pure a) ⊥ := ⟨by simp⟩
+instance tendsto_Ioo_pure_bot {a : α} : tendsto_Ixx_class Ioo (pure a) ⊥ := ⟨by simp⟩
 
 end partial_order
 
@@ -225,7 +218,7 @@ end
 
 lemma tendsto.interval {l : filter α} [tendsto_Ixx_class Icc l l] {f g : β → α} {lb : filter β}
   (hf : tendsto f lb l) (hg : tendsto g lb l) :
-  tendsto (λ x, [f x, g x]) lb (l.lift' powerset) :=
+  tendsto (λ x, [f x, g x]) lb l.small_sets :=
 tendsto_Ixx_class.tendsto_Ixx.comp $ hf.prod_mk hg
 
 end linear_order