uniformCauchySeqOn_iff_uniformCauchySeqOnFilter

English

UniformCauchySeqOn F p s is equivalent to UniformCauchySeqOnFilter F p (principal s).

Русский

UniformCauchySeqOn F p s эквивалентна UniformCauchySeqOnFilter F p (principal s).

LaTeX

$$$UniformCauchySeqOn F p s \iff UniformCauchySeqOnFilter F p (\\mathcal{P}s)$$$

Lean4

theorem uniformCauchySeqOn_iff_uniformCauchySeqOnFilter :
    UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s) :=
  by
  simp only [UniformCauchySeqOn, UniformCauchySeqOnFilter]
  refine forall₂_congr fun u hu => ?_
  rw [eventually_prod_principal_iff]

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