cauchyFilter_eq — Mathlib

English

For complete separated α, lim f.1 = lim g.1 iff Inseparable f g.

Русский

Для полного разделимого пространства α, равны лимитные предельные фильтры lim f и lim g тогда, когда Inseparable f g.

LaTeX

$$$\\text{CauchyFilter.cauchyFilter_eq}\\;: \\forall {f,g},\\ haveI := f.2.1.nonempty;\\ lim f.1 = lim g.1 \\iff Inseparable f g$$$

Lean4

theorem cauchyFilter_eq {α : Type*} [UniformSpace α] [CompleteSpace α] [T0Space α] {f g : CauchyFilter α} :
    haveI := f.2.1.nonempty;
    lim f.1 = lim g.1 ↔ Inseparable f g :=
  by rw [← inseparable_iff_eq, inseparable_lim_iff]

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