α✝ : Type ?u.79050
β : Type u_2
γ : Type ?u.79056
ι : Type ?u.79059
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_1
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f
α✝ : Type ?u.79050
β : Type u_2
γ : Type ?u.79056
ι : Type ?u.79059
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_1
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ limsup u f = limsup v f
rw [limsup_eq]
case e_a.h
α✝ : Type ?u.79050
β : Type u_2
γ : Type ?u.79056
ι : Type ?u.79059
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_1
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
⊢ b ∈ {a | ∀ᶠ (n : α) in f, u n ≤ a} ↔ b ∈ {a | ∀ᶠ (n : β) in map v f, n ≤ a}
α✝ : Type ?u.79050
β : Type u_2
γ : Type ?u.79056
ι : Type ?u.79059
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_1
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f
congr with b
no goals
case e_a.h
α✝ : Type ?u.79050
β : Type u_2
γ : Type ?u.79056
ι : Type ?u.79059
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_1
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
⊢ b ∈ {a | ∀ᶠ (n : α) in f, u n ≤ a} ↔ b ∈ {a | ∀ᶠ (n : β) in map v f, n ≤ a}
exact eventually_congr (h.mono fun x hx => by simp [hx])
no goals
α✝ : Type ?u.79050
β : Type u_2
γ : Type ?u.79056
ι : Type ?u.79059
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_1
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
x : α
hx : u x = v x
⊢ u x ≤ b ↔ v x ∈ {x | (fun n => n ≤ b) x}
simp [hx]