α✝ : Type u
β : Type v
γ : Type w
inst✝¹⁰ : TopologicalSpace α✝
inst✝⁹ : TopologicalSpace β
inst✝⁸ : LinearOrder α✝
inst✝⁷ : LinearOrder β
inst✝⁶ : OrderTopology α✝
inst✝⁵ : OrderTopology β
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : ¬x ∈ Ioo y x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
α✝ : Type u
β : Type v
γ : Type w
inst✝¹⁰ : TopologicalSpace α✝
inst✝⁹ : TopologicalSpace β
inst✝⁸ : LinearOrder α✝
inst✝⁷ : LinearOrder β
inst✝⁶ : OrderTopology α✝
inst✝⁵ : OrderTopology β
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
have hx : x ∉ Ioo y x := fun h => (lt_irrefl x h.2).elim
α✝ : Type u
β : Type v
γ : Type w
inst✝¹⁰ : TopologicalSpace α✝
inst✝⁹ : TopologicalSpace β
inst✝⁸ : LinearOrder α✝
inst✝⁷ : LinearOrder β
inst✝⁶ : OrderTopology α✝
inst✝⁵ : OrderTopology β
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : ¬x ∈ Ioo y x
ht : Set.Nonempty (Ioo y x)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
α✝ : Type u
β : Type v
γ : Type w
inst✝¹⁰ : TopologicalSpace α✝
inst✝⁹ : TopologicalSpace β
inst✝⁸ : LinearOrder α✝
inst✝⁷ : LinearOrder β
inst✝⁶ : OrderTopology α✝
inst✝⁵ : OrderTopology β
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : ¬x ∈ Ioo y x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
have ht : Set.Nonempty (Ioo y x) := nonempty_Ioo.2 hy
case intro
α✝ : Type u
β : Type v
γ : Type w
inst✝¹⁰ : TopologicalSpace α✝
inst✝⁹ : TopologicalSpace β
inst✝⁸ : LinearOrder α✝
inst✝⁷ : LinearOrder β
inst✝⁶ : OrderTopology α✝
inst✝⁵ : OrderTopology β
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : ¬x ∈ Ioo y x
ht : Set.Nonempty (Ioo y x)
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ Ioo y x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
α✝ : Type u
β : Type v
γ : Type w
inst✝¹⁰ : TopologicalSpace α✝
inst✝⁹ : TopologicalSpace β
inst✝⁸ : LinearOrder α✝
inst✝⁷ : LinearOrder β
inst✝⁶ : OrderTopology α✝
inst✝⁵ : OrderTopology β
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : ¬x ∈ Ioo y x
ht : Set.Nonempty (Ioo y x)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
rcases(isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_not_mem hx ht with ⟨u, hu⟩
no goals
case intro
α✝ : Type u
β : Type v
γ : Type w
inst✝¹⁰ : TopologicalSpace α✝
inst✝⁹ : TopologicalSpace β
inst✝⁸ : LinearOrder α✝
inst✝⁷ : LinearOrder β
inst✝⁶ : OrderTopology α✝
inst✝⁵ : OrderTopology β
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
hx : ¬x ∈ Ioo y x
ht : Set.Nonempty (Ioo y x)
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ Ioo y x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
exact ⟨u, hu.1, hu.2.2.symm⟩