mono — Mathlib

English

If a power-series is valid on a ball with radius s, and t is contained in s, it remains valid on t with the same radius.

Русский

Если степенной ряд верен на шаре радиуса s, и t ⊆ s, то он сохраняется на t с тем же радиусом.

LaTeX

$$$HasFPowerSeriesWithinOnBall f p s x r \\to (t \\subset s) \\Rightarrow HasFPowerSeriesWithinOnBall f p t x r$$$

Lean4

theorem mono (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : t ⊆ s) : HasFPowerSeriesWithinOnBall f p t x r
    where
  r_le := hf.r_le
  r_pos := hf.r_pos
  hasSum hy h'y := hf.hasSum (insert_subset_insert h hy) h'y

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