termω — Mathlib

English

If h : HasFTaylorSeriesUpToOn n f p s and m ≤ n, then HasFTaylorSeriesUpToOn m f p s holds.

Русский

Если h : HasFTaylorSeriesUpToOn n f p s и m ≤ n, то HasFTaylorSeriesUpToOn m f p s выполняется.

LaTeX

$$$HasFTaylorSeriesUpToOn\ n\ f\ p\ s \to m \le n \Rightarrow HasFTaylorSeriesUpToOn m f p s$$$

Lean4

/-- Smoothness exponent for analytic functions. -/
@[scoped term_parser 1000]
public meta def termω : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ContDiff.termω 1024 (ParserDescr.symbol✝ "ω")

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