case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ b ∈ closure (Ioo a b)

case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ extendFrom (Ioo a b) f b = lb
apply extendFrom_eq
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ b ∈ Icc a b
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ b ∈ closure (Ioo a b)
rw [closure_Ioo hab.ne]
no goals
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ b ∈ Icc a b
simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc]
no goals
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)
simpa [hab]