Comparing smoothness orders with infinity

The outer top of WithTop ℕ∞ is analytic regularity. Every other order is at most smooth regularity. This characterization lets simplification handle finite derivative orders without depending on their numeral representation.

@[simp]

theorem NavierStokesAndEuler.le_infinity_iff_ne_top (n : WithTop ℕ∞) : n ≤ ↑⊤ ↔ n ≠ ⊤