α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
this : ContinuousOn f (Ioo b a) → Tendsto f (𝓝[Ioi b] b) (𝓝 lb) → ContinuousOn (extendFrom (Ioo b a) f) (Ico b a)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
have := @continuousOn_Ico_extendFrom_Ioo αᵒᵈ _ _ _ _ _ _ _ f _ _ lb hab
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
this :
  ContinuousOn f (↑OrderDual.ofDual ⁻¹' Ioo a b) →
    Tendsto f (𝓝[↑OrderDual.ofDual ⁻¹' Iio b] b) (𝓝 lb) →
      ContinuousOn (extendFrom (↑OrderDual.ofDual ⁻¹' Ioo a b) f) (↑OrderDual.ofDual ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
this : ContinuousOn f (Ioo b a) → Tendsto f (𝓝[Ioi b] b) (𝓝 lb) → ContinuousOn (extendFrom (Ioo b a) f) (Ico b a)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
erw [dual_Ico, dual_Ioi, dual_Ioo] at this
no goals
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
this :
  ContinuousOn f (↑OrderDual.ofDual ⁻¹' Ioo a b) →
    Tendsto f (𝓝[↑OrderDual.ofDual ⁻¹' Iio b] b) (𝓝 lb) →
      ContinuousOn (extendFrom (↑OrderDual.ofDual ⁻¹' Ioo a b) f) (↑OrderDual.ofDual ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)
exact this hf hb