contDiffWithinAt_iff_forall_nat_le

English

For n an ENat, ContDiffWithinAt 𝕜 (WithTop.some n) f s x is equivalent to the statement that all natural orders m with m ≤ n satisfy ContDiffWithinAt 𝕜 m f s x.

Русский

Для n ∈ ENat ContDiffWithinAt 𝕜 (WithTop.some n) f s x эквивалентно тому, что для каждого натурального m, удовлетворяющего m ≤ n, выполняется ContDiffWithinAt 𝕜 m f s x.

LaTeX

$$$ ContDiffWithinAt 𝕜 (WithTop.some n) f s x \\iff \\forall m : \\mathbb{N}, m \\le n \\Rightarrow ContDiffWithinAt 𝕜 m f s x$$

Lean4

theorem contDiffWithinAt_iff_forall_nat_le {n : ℕ∞} :
    ContDiffWithinAt 𝕜 n f s x ↔ ∀ m : ℕ, ↑m ≤ n → ContDiffWithinAt 𝕜 m f s x :=
  ⟨fun H _ hm => H.of_le (mod_cast hm), fun H m hm => H m hm _ le_rfl⟩

Похожие утверждения