English
If minSmoothness 𝕜 m ≤ n for some m, there exists n' with minSmoothness 𝕜 m ≤ n' ≤ n and n' ≠ ∞.
Русский
Если minSmoothness 𝕜 m ≤ n для некоторого m, существует n' с minSmoothness 𝕜 m ≤ n' ≤ n и n' ≠ ∞.
LaTeX
$$$$ \\exists n',\\; \\minSmoothness_{\\mathbb{k}}(m) \\le n' \\le n \\;\\land\\; n' \\neq \\infty. $$$$
Lean4
/-- If `minSmoothness 𝕜 m ≤ n` for some (finite) integer `m`, then one can
find `n' ∈ [minSmoothness 𝕜 m, n]` which is not `∞`: over `ℝ` or `ℂ`, just take `m`, and otherwise
just take `ω`. The interest of this technical lemma is that, if a function is `C^{n'}` at a point
for `n' ≠ ∞`, then it is `C^{n'}` on a neighborhood of the point (this property fails only
in `C^∞` smoothness, see `ContDiffWithinAt.contDiffOn`). -/
theorem exist_minSmoothness_le_ne_infty {n : WithTop ℕ∞} {m : ℕ} (hm : minSmoothness 𝕜 m ≤ n) :
∃ n', minSmoothness 𝕜 m ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞ :=
by
simp only [minSmoothness] at hm ⊢
split_ifs with h
· simp only [h, ↓reduceIte] at hm
exact ⟨m, le_rfl, hm, by simp⟩
· simp only [h, ↓reduceIte, top_le_iff] at hm
refine ⟨ω, le_rfl, by simp [hm], by simp⟩
