exact hxy ▸ hs x (ht hxt)
case intro.intro.intro.intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y✝ : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y✝)
y' : β
hy' : y✝ < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
t : Set α
ht : t ⊆ s
y : β
x : α
hxt : x ∈ t
hxy : f x = y
⊢ y ≤ y'
no goals