case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsBoundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae ν) f

case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsCoboundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ essInf f ν ≤ essInf f μ
refine' liminf_le_liminf_of_le (Measure.ae_le_iff_absolutelyContinuous.mpr hμν) _ _
no goals
case refine'_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsBoundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae ν) f

case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsCoboundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f
all_goals isBoundedDefault
no goals
case refine'_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : MeasureTheory.Measure α
inst✝ : CompleteLattice β
f : α → β
hμν : μ ≪ ν
⊢ IsCoboundedUnder (fun x x_1 => x ≥ x_1) (Measure.ae μ) f
isBoundedDefault