ofSets_filter_eq_generate — Mathlib

English

The filter generated by s equals the filter generated by the OfSets basis; i.e., filter equals generate s.

Русский

Фильтр, образованный по множеству s, эквивалентен фильтру, генерируемому базисом OfSets; то есть filter = generate s.

LaTeX

$$(FilterBasis.ofSets s).filter = generate s.$$

Lean4

theorem ofSets_filter_eq_generate (s : Set (Set α)) : (FilterBasis.ofSets s).filter = generate s := by
  rw [← (FilterBasis.ofSets s).generate, FilterBasis.ofSets_sets, ← generate_eq_generate_inter]

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