f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = 0
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = 0
have : ContinuousOn f (Ioo a b) := fun x hx => (hff' x hx).continuousAt.continuousWithinAt
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = 0
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = 0
have hcont := continuousOn_Icc_extendFrom_Ioo hab.ne this hfa hfb
case intro.intro
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
c : ℝ
hc : c ∈ Ioo a b
hcextr : IsLocalExtr (extendFrom (Ioo a b) f) c
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = 0
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = 0
obtain ⟨c, hc, hcextr⟩ : ∃ c ∈ Ioo a b, IsLocalExtr (extendFrom (Ioo a b) f) c := by
  apply exists_local_extr_Ioo _ hab hcont
  rw [eq_lim_at_right_extendFrom_Ioo hab hfb]
  exact eq_lim_at_left_extendFrom_Ioo hab hfa
case intro.intro
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
c : ℝ
hc : c ∈ Ioo a b
hcextr : IsLocalExtr (extendFrom (Ioo a b) f) c
⊢ f' c = 0
case intro.intro
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
c : ℝ
hc : c ∈ Ioo a b
hcextr : IsLocalExtr (extendFrom (Ioo a b) f) c
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = 0
use c, hc
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
c : ℝ
hc : c ∈ Ioo a b
hcextr : IsLocalExtr (extendFrom (Ioo a b) f) c
⊢ extendFrom (Ioo a b) f =ᶠ[𝓝 c] f
case intro.intro
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
c : ℝ
hc : c ∈ Ioo a b
hcextr : IsLocalExtr (extendFrom (Ioo a b) f) c
⊢ f' c = 0
apply (hcextr.congr _).hasDerivAt_eq_zero (hff' c hc)
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
c : ℝ
hc : c ∈ Ioo a b
hcextr : IsLocalExtr (extendFrom (Ioo a b) f) c
⊢ ∃ s, s ∈ 𝓝 c ∧ EqOn (extendFrom (Ioo a b) f) f s
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
c : ℝ
hc : c ∈ Ioo a b
hcextr : IsLocalExtr (extendFrom (Ioo a b) f) c
⊢ extendFrom (Ioo a b) f =ᶠ[𝓝 c] f
rw [eventuallyEq_iff_exists_mem]
no goals
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
c : ℝ
hc : c ∈ Ioo a b
hcextr : IsLocalExtr (extendFrom (Ioo a b) f) c
⊢ ∃ s, s ∈ 𝓝 c ∧ EqOn (extendFrom (Ioo a b) f) f s
exact ⟨Ioo a b, Ioo_mem_nhds hc.1 hc.2, extendFrom_extends this⟩
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ extendFrom (Ioo a b) f a = extendFrom (Ioo a b) f b
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ ∃ c, c ∈ Ioo a b ∧ IsLocalExtr (extendFrom (Ioo a b) f) c
apply exists_local_extr_Ioo _ hab hcont
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ extendFrom (Ioo a b) f a = l
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ extendFrom (Ioo a b) f a = extendFrom (Ioo a b) f b
rw [eq_lim_at_right_extendFrom_Ioo hab hfb]
no goals
f f' : ℝ → ℝ
a b l : ℝ
hab : a < b
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
this : ContinuousOn f (Ioo a b)
hcont : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b)
⊢ extendFrom (Ioo a b) f a = l
exact eq_lim_at_left_extendFrom_Ioo hab hfa