inseparable_iff_of_le_nhds — Mathlib

English

If f,g are CauchyFilters with f.1 ≤ nhds a and g.1 ≤ nhds b, then Inseparable a b iff Inseparable f g.

Русский

Если f,g — фильтры Коши с f.1 ≤ nhds a и g.1 ≤ nhds b, то inseparable a b эквивалентно inseparable f g.

LaTeX

$$$\\forall a,b,\\ (ha:\\, f.1\\le nhds(a))\\ (hb:\\, g.1\\le nhds(b))\\Rightarrow Inseparable(a,b)\\iff Inseparable(f,g)$$$

Lean4

theorem inseparable_iff_of_le_nhds {f g : CauchyFilter α} {a b : α} (ha : f.1 ≤ 𝓝 a) (hb : g.1 ≤ 𝓝 b) :
    Inseparable a b ↔ Inseparable f g := by
  rw [← tendsto_id'] at ha hb
  rw [inseparable_iff, (ha.comp tendsto_fst).inseparable_iff_uniformity (hb.comp tendsto_snd)]
  simp only [Function.comp_apply, id_eq, Prod.mk.eta, ← Function.id_def, tendsto_id']

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