inseparable_lim_iff — Mathlib

English

Under [CompleteSpace α], for f,g ∈ CauchyFilter α, Inseparable (lim f.1) (lim g.1) iff Inseparable f g.

Русский

При [CompleteSpace α] для f,g ∈ CauchyFilter α: inseparable(lim f.1) (lim g.1) ⇔ inseparable f g.

LaTeX

$$$[CompleteSpace\\alpha] \\ {f,g:\\ CauchyFilter(\\alpha)}: Inseparable(\\lim f.1)(\\lim g.1) \\iff Inseparable(f,g)$$$

Lean4

theorem inseparable_lim_iff [CompleteSpace α] {f g : CauchyFilter α} :
    haveI := f.2.1.nonempty;
    Inseparable (lim f.1) (lim g.1) ↔ Inseparable f g :=
  inseparable_iff_of_le_nhds f.2.le_nhds_lim g.2.le_nhds_lim

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