contDiffOn_all_iff_nat — Mathlib

English

Equivalence between ENat cast orders and Nat orders for ContDiffOn.

Русский

Эквивалентность между ENat-приведёнными порядками и натуральными порядками для ContDiffOn.

LaTeX

$$$\forall f,s: ContDiffOn 𝕜 (WithTop.some n) f s \Leftrightarrow ContDiffOn 𝕜 n.cast f s$$$

Lean4

theorem contDiffOn_all_iff_nat : (∀ (n : ℕ∞), ContDiffOn 𝕜 n f s) ↔ ∀ n : ℕ, ContDiffOn 𝕜 n f s :=
  by
  refine ⟨fun H n => H n, ?_⟩
  rintro H (_ | n)
  exacts [contDiffOn_infty.2 H, H n]

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