cauchyFilter_gen — Mathlib

English

If s ⊆ X×X is transitive, then the generated CauchyFilter.gen(s) is transitive.

Русский

Пусть s ⊆ X×X транзитивно; тогда CauchyFilter.gen(s) транзитивен.

LaTeX

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

Lean4

theorem cauchyFilter_gen {s : Set (X × X)} (hs : IsTransitiveRel s) : IsTransitiveRel (CauchyFilter.gen s) :=
  by
  simp only [IsTransitiveRel, CauchyFilter.gen, mem_setOf_eq]
  intro f g h hfg hgh
  exact hs.mem_filter_prod_trans hfg hgh

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