cauchyFilter_gen — Mathlib

English

Let s be a symmetric relation on a uniform space X. Then the Cauchy filter generated by s is symmetric; i.e., IsSymmetricRel(CauchyFilter.gen(s)).

Русский

Пусть s ⊆ X×X — симметричное отношение на равномерном пространстве X. Тогда порожденный им фильтр Коши, CauchyFilter.gen(s), тоже симметричен.

LaTeX

$$$IsSymmetricRel\big( \mathrm{CauchyFilter.gen}(s) \big)$$$

Lean4

theorem cauchyFilter_gen {s : Set (X × X)} (h : IsSymmetricRel s) : IsSymmetricRel (CauchyFilter.gen s) := by
  simp [IsSymmetricRel, CauchyFilter.gen, h.mem_filter_prod_comm]

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