case refine'_1
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f

case refine'_2
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f

case refine'_3
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) fun x => ↑g (f x)

case refine'_4
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) fun x => ↑g (f x)
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ ↑g (essSup f μ) = essSup (fun x => ↑g (f x)) μ
refine' OrderIso.limsup_apply g _ _ _ _
no goals
case refine'_1
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f

case refine'_2
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) f

case refine'_3
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) fun x => ↑g (f x)

case refine'_4
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) fun x => ↑g (f x)
all_goals isBoundedDefault
no goals
case refine'_4
α : Type u_1
β : Type u_3
m✝ : MeasurableSpace α
μ✝ ν : MeasureTheory.Measure α
inst✝¹ : CompleteLattice β
m : MeasurableSpace α
γ : Type u_2
inst✝ : CompleteLattice γ
f : α → β
μ : MeasureTheory.Measure α
g : β ≃o γ
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) (Measure.ae μ) fun x => ↑g (f x)
isBoundedDefault