instTopologicalSpaceA — Mathlib

English

Every object X of Compactum carries a topology on its underlying type A.

Русский

Каждый объект X компактума имеет топологию на своей базовой множестве A.

LaTeX

$$$\\text{TopologicalSpace } X.A$$$

Lean4

instance {X : Compactum} : TopologicalSpace X
    where
  IsOpen U := ∀ F : Ultrafilter X, X.str F ∈ U → U ∈ F
  isOpen_univ _ _ := Filter.univ_sets _
  isOpen_inter _ _ h3 h4 _ h6 := Filter.inter_sets _ (h3 _ h6.1) (h4 _ h6.2)
  isOpen_sUnion := fun _ h1 _ ⟨T, hT, h2⟩ => mem_of_superset (h1 T hT _ h2) (Set.subset_sUnion_of_mem hT)

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