principal_isMeasurablyGenerated_iff

English

The principal filter of a set s is measurably generated if and only if s is measurable.

Русский

Фильтр-деление по множеству s измеримо порожден тогда и только тогда, когда s измеримо.

LaTeX

$$$MeasurablyGenerated(\\\\mathcal{P} s) \\\\Leftrightarrow MeasurableSet s$$$

Lean4

theorem principal_isMeasurablyGenerated_iff {s : Set α} : IsMeasurablyGenerated (𝓟 s) ↔ MeasurableSet s :=
  by
  refine ⟨?_, fun hs => ⟨fun t ht => ⟨s, mem_principal_self s, hs, ht⟩⟩⟩
  rintro ⟨hs⟩
  rcases hs (mem_principal_self s) with ⟨t, ht, htm, hts⟩
  have : t = s := hts.antisymm ht
  rwa [← this]

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