generate_eq_generate_inter — Mathlib

English

generate s equals generate of the images by finite intersections; i.e., interchanging representations.

Русский

generate s равен generate изображения через конечные пересечения; тождественность представлений.

LaTeX

$$generate s = generate (sInter '' {t | Finite t ∧ t ⊆ s}).$$

Lean4

theorem generate_eq_generate_inter (s : Set (Set α)) : generate s = generate (sInter '' {t | Set.Finite t ∧ t ⊆ s}) :=
  by rw [← FilterBasis.ofSets_sets, FilterBasis.generate, ← (hasBasis_generate s).filter_eq]; rfl

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