[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
[PROOFSTEP]
apply continuousOn_extendFrom
[GOAL]
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ Icc a b ⊆ closure (Ioo a b)
[PROOFSTEP]
rw [closure_Ioo hab]
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
⊢ ∀ (x : α), x ∈ Icc a b → ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
intro x x_in
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
x : α
x_in : x ∈ Icc a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)
[GOAL]
case hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la lb : β
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
x : α
hab : x ≠ b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[Ioi x] x) (𝓝 la)
x_in : x ∈ Icc x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
[PROOFSTEP]
exact ⟨la, ha.mono_left <| nhdsWithin_mono _ Ioo_subset_Ioi_self⟩
[GOAL]
case hf.inr.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a : α
la lb : β
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
x : α
hab : a ≠ x
hf : ContinuousOn f (Ioo a x)
hb : Tendsto f (𝓝[Iio x] x) (𝓝 lb)
x_in : x ∈ Icc a x
⊢ ∃ y, Tendsto f (𝓝[Ioo a x] x) (𝓝 y)
[PROOFSTEP]
exact ⟨lb, hb.mono_left <| nhdsWithin_mono _ Ioo_subset_Iio_self⟩
[GOAL]
case hf.inr.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la lb : β
hab : a ≠ b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 lb)
x : α
x_in : x ∈ Icc a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
exact ⟨f x, hf x h⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ extendFrom (Ioo a b) f a = la
[PROOFSTEP]
apply extendFrom_eq
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ a ∈ closure (Ioo a b)
[PROOFSTEP]
rw [closure_Ioo hab.ne]
[GOAL]
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ a ∈ Icc a b
[PROOFSTEP]
simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc]
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
la : β
hab : a < b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ Tendsto f (𝓝[Ioo a b] a) (𝓝 la)
[PROOFSTEP]
simpa [hab]
[GOAL]
α : 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
[PROOFSTEP]
apply extendFrom_eq
[GOAL]
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)
[PROOFSTEP]
rw [closure_Ioo hab.ne]
[GOAL]
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
[PROOFSTEP]
simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc]
[GOAL]
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)
[PROOFSTEP]
simpa [hab]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ico a b)
[PROOFSTEP]
apply continuousOn_extendFrom
[GOAL]
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ Ico a b ⊆ closure (Ioo a b)
[PROOFSTEP]
rw [closure_Ioo hab.ne]
[GOAL]
case hB
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ Ico a b ⊆ Icc a b
[PROOFSTEP]
exact Ico_subset_Icc_self
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
⊢ ∀ (x : α), x ∈ Ico a b → ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
intro x x_in
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
x : α
x_in : x ∈ Ico a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
rcases eq_left_or_mem_Ioo_of_mem_Ico x_in with (rfl | h)
[GOAL]
case hf.inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la : β
x : α
hab : x < b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[Ioi x] x) (𝓝 la)
x_in : x ∈ Ico x b
⊢ ∃ y, Tendsto f (𝓝[Ioo x b] x) (𝓝 y)
[PROOFSTEP]
use la
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
b : α
la : β
x : α
hab : x < b
hf : ContinuousOn f (Ioo x b)
ha : Tendsto f (𝓝[Ioi x] x) (𝓝 la)
x_in : x ∈ Ico x b
⊢ Tendsto f (𝓝[Ioo x b] x) (𝓝 la)
[PROOFSTEP]
simpa [hab]
[GOAL]
case hf.inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
la : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 la)
x : α
x_in : x ∈ Ico a b
h : x ∈ Ioo a b
⊢ ∃ y, Tendsto f (𝓝[Ioo a b] x) (𝓝 y)
[PROOFSTEP]
exact ⟨f x, hf x h⟩
[GOAL]
α : 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)
[PROOFSTEP]
have := @continuousOn_Ico_extendFrom_Ioo αᵒᵈ _ _ _ _ _ _ _ f _ _ lb hab
[GOAL]
α : 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)
[PROOFSTEP]
erw [dual_Ico, dual_Ioi, dual_Ioo] at this 
[GOAL]
α : 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)
[PROOFSTEP]
exact this hf hb
