uniformCauchySeqOnFilter — Mathlib

English

If UniformCauchySeqOnFilter F p p' holds and p'' ≤ p, then UniformCauchySeqOnFilter F p'' p' holds as well.

Русский

Если UniformCauchySeqOnFilter F p p' выполняется и p'' ≤ p, тогда верно UniformCauchySeqOnFilter F p'' p'.

LaTeX

$$$UniformCauchySeqOnFilter F p p' \to p'' \le p \Rightarrow UniformCauchySeqOnFilter F p'' p'$$$

Lean4

theorem uniformCauchySeqOnFilter (hF : UniformCauchySeqOn F p s) : UniformCauchySeqOnFilter F p (𝓟 s) := by
  rwa [← uniformCauchySeqOn_iff_uniformCauchySeqOnFilter]

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