ultrafilterBasis_is_basis — Mathlib

English

The set ultrafilterBasis α forms a basis for the topology on Ultrafilter α; it satisfies the basis axioms for neighborhoods and finite intersections, etc.

Русский

Набор ultrafilterBasis α образует базис топологии на Ultrafilter α и удовлетворяет аксиомам базиса.

LaTeX

$$$\\mathrm{IsTopologicalBasis}(\\mathrm{ultrafilterBasis}(\\alpha)).$$$

Lean4

theorem ultrafilterBasis_is_basis : TopologicalSpace.IsTopologicalBasis (ultrafilterBasis α) :=
  ⟨by
    rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ u ⟨ua, ub⟩
    refine ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv ↦ ⟨?_, ?_⟩⟩ <;> apply mem_of_superset hv <;>
      simp [inter_subset_right],
    eq_univ_of_univ_subset <| subset_sUnion_of_mem <| ⟨univ, eq_univ_of_forall fun _ ↦ univ_mem⟩, rfl⟩

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