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)

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)
α : 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)
apply continuousOn_extendFrom
no goals
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)
rw [closure_Ioo hab]
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)
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)
intro x x_in
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)

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)

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)
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)
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc x_in with (rfl | rfl | h)
no goals
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)
exact ⟨la, ha.mono_left <| nhdsWithin_mono _ Ioo_subset_Ioi_self⟩
no goals
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)
exact ⟨lb, hb.mono_left <| nhdsWithin_mono _ Ioo_subset_Iio_self⟩
no goals
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)
exact ⟨f x, hf x h⟩