instIsMeasurablyGeneratedCocompactOfR1Space

English

In every R1-space, the cocompact filter is measurably generated.

Русский

В любом R1-пространстве коккомпактный фильтр измеримо порожден.

LaTeX

$$$(\text{Filter.cocompact } \alpha).IsMeasurablyGenerated$ \text{ for } \text{R1-space } \alpha$.$$

Lean4

instance [R1Space α] : IsMeasurablyGenerated (cocompact α) where
  exists_measurable_subset := by
    intro _ hs
    obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
    exact
      ⟨(closure t)ᶜ, ht.closure.compl_mem_cocompact, isClosed_closure.measurableSet.compl,
        (compl_subset_compl.2 subset_closure).trans hts⟩

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