English
Another variant of succ_iff_hasFDerivWithinAt with alternative formation.
Русский
Альтернативная форма succ_iff_hasFDerivWithinAt.
LaTeX
$$$\text{ContDiffWithinAt}_{\mathbb{K}}(n+1,f;s;x) \iff \exists u \in 𝓝[insert x s] x, \; u \subset insert x s \land \cdots$$$
Lean4
theorem contDiffOn' (hm : m ≤ n) (h' : m = ∞ → n = ω) (h : ContDiffWithinAt 𝕜 n f s x) :
∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 m f (insert x s ∩ u) :=
by
rcases eq_or_ne n ω with rfl | hn
· obtain ⟨t, ht, p, hp, h'p⟩ := h
rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩
rw [inter_comm] at hut
refine ⟨u, huo, hxu, ?_⟩
suffices ContDiffOn 𝕜 ω f (insert x s ∩ u) from this.of_le le_top
intro y hy
refine ⟨insert x s ∩ u, ?_, p, hp.mono hut, fun i ↦ (h'p i).mono hut⟩
simp only [insert_eq_of_mem, hy, self_mem_nhdsWithin]
·
match m with
| ω => simp [hn] at hm
| ∞ => exact (hn (h' rfl)).elim
| (m : ℕ) =>
rcases contDiffWithinAt_nat.1 (h.of_le hm) with ⟨t, ht, p, hp⟩
rcases mem_nhdsWithin.1 ht with ⟨u, huo, hxu, hut⟩
rw [inter_comm] at hut
exact ⟨u, huo, hxu, (hp.mono hut).contDiffOn⟩
