ofSets_sets — Mathlib

English

The FilterBasis.ofSets s is a basis whose sets are generated by finite intersections of members of s.

Русский

FilterBasis.ofSets s образует базис, чьи множества получаются как конечные пересечения элементов s.

LaTeX

$$FilterBasis.ofSets s .sets = { ∩ t | t finite, t ⊆ s }.$$

Lean4

theorem ofSets_sets (s : Set (Set α)) : (FilterBasis.ofSets s).sets = sInter '' {t | Set.Finite t ∧ t ⊆ s} :=
  rfl

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