hasBasis_cocompact — Mathlib

English

A set belongs to cocompact X if and only if there exists a compact t with t ⊆ X \\ s.

Русский

Множество принадлежит кокомбоплекту X тогда и только тогда, когда существует компактное t, такое что t ⊆ X \\ s.

LaTeX

$$$s \\in \\operatorname{cocompact}(X) \\iff \\exists t, \\operatorname{IsCompact}(t) \\land t^{c} \\subseteq s$$$

Lean4

theorem hasBasis_cocompact : (cocompact X).HasBasis IsCompact compl :=
  hasBasis_biInf_principal'
    (fun s hs t ht =>
      ⟨s ∪ t, hs.union ht, compl_subset_compl.2 subset_union_left, compl_subset_compl.2 subset_union_right⟩)
    ⟨∅, isCompact_empty⟩

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