α : Type u_1
β : Type ?u.5738175
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
f✝ : α → ℝ≥0∞
f : α → ℝ≥0
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
r : ℝ≥0∞
⊢ (∀ (i : ℝ≥0), (i ∈ fun x => sets (map f (Measure.ae μ)) {x_1 | x_1 ≤ x}) → r ≤ ↑i) ↔
    ∀ (r_1 : ℝ≥0), (∀ᵐ (a : α) ∂μ, f a ≤ r_1) → r ≤ ↑r_1
α : Type u_1
β : Type ?u.5738175
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
f✝ : α → ℝ≥0∞
f : α → ℝ≥0
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
r : ℝ≥0∞
⊢ (r ≤
      ⨅ (a : ℝ≥0) (_ : a ∈ fun x => sets (map f (Measure.ae μ)) {x_1 | (fun x_2 => (fun x x_3 => x ≤ x_3) x_2 x) x_1}),
        ↑a) ↔
    r ≤ essSup (fun x => ↑(f x)) μ
simp [essSup, limsup, limsSup, eventually_map, ENNReal.forall_ennreal]
no goals
α : Type u_1
β : Type ?u.5738175
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
f✝ : α → ℝ≥0∞
f : α → ℝ≥0
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f
r : ℝ≥0∞
⊢ (∀ (i : ℝ≥0), (i ∈ fun x => sets (map f (Measure.ae μ)) {x_1 | x_1 ≤ x}) → r ≤ ↑i) ↔
    ∀ (r_1 : ℝ≥0), (∀ᵐ (a : α) ∂μ, f a ≤ r_1) → r ≤ ↑r_1
rfl