inseparable_iff

Mathlib.Topology.UniformSpace.Completion

URI: https://scilib.ai/kg/mathlib#CauchyFilter.inseparable_iff

English

For Cauchy filters f,g, Inseparable f g iff f.1 ×ˢ g.1 ≤ 𝓤 α.

Русский

Для фильтров Коши f,g: inseparable(f,g) эквивалентно f.1 ×ˢ g.1 ≤ 𝓤 α.

LaTeX

$$$\\operatorname{Inseparable}(f,g) \\iff f.1 \\timesˢ g.1 \\le 𝓤(\\alpha)$$$

Lean4

theorem inseparable_iff {f g : CauchyFilter α} : Inseparable f g ↔ f.1 ×ˢ g.1 ≤ 𝓤 α :=
  (basis_uniformity (basis_sets _)).inseparable_iff_uniformity

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru