α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ limsup (fun x => ↑g (u x)) f ≤ ↑g (limsup u f)
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑g (limsup u f) = limsup (fun x => ↑g (u x)) f
refine' le_antisymm ((OrderIso.to_galoisConnection g).l_limsup_le hgu hu_co) _
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑g (↑(symm g) (limsup (fun x => ↑g (u x)) f)) ≤ ↑g (limsup u f)
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ limsup (fun x => ↑g (u x)) f ≤ ↑g (limsup u f)
rw [← g.symm.symm_apply_apply <| limsup (fun x => g (u x)) f, g.symm_symm]
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup u f
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑g (↑(symm g) (limsup (fun x => ↑g (u x)) f)) ≤ ↑g (limsup u f)
refine' g.monotone _
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup u f
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup u f
have hf : u = fun i => g.symm (g (u i)) := funext fun i => (g.symm_apply_apply (u i)).symm
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup (fun i => ↑(symm g) (↑g (u i))) f
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup u f
nth_rw 2 [hf]
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑(symm g) (↑g (u x))
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup (fun i => ↑(symm g) (↑g (u i))) f
refine' (OrderIso.to_galoisConnection g.symm).l_limsup_le _ hgu_co
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => u x
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑(symm g) (↑g (u x))
simp_rw [g.symm_apply_apply]
no goals
α : Type u_3
β : Type u_2
γ✝ : Type ?u.207655
ι : Type ?u.207658
γ : Type u_1
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => u x
exact hu