instCountablySeparatedElemOfHasCountableSeparatingOnIsOpen

English

Measurable sets can be generated from open sets by complementation and countable unions under the usual induction framework.

Русский

Измеримые множества порождаются открытыми множествами через дополнение и счётные объединения в рамках обычной индукции.

LaTeX

$$$$ \forall C : (s \to \text{MeasurableSet } s \to \text{Prop}),\ (\forall U\,(hU:IsOpen U), C(U)) \land (\forall t\,(ht:\text{MeasurableSet } t), C(t) \Rightarrow C(t^{c})) \land (\forall f: \mathbb{N} \to s), (\text{Pairwise Disjoint on } f) \Rightarrow (\forall hf, (\forall i, \text{MeasurableSet}(f i)) \Rightarrow (\forall i, C(f i) (hf i)) \Rightarrow C(\bigcup_i f i)) \Rightarrow \forall t\, (ht: \text{MeasurableSet } t), C(t). $$$$

Lean4

instance (priority := 1000) {s : Set α} [h : HasCountableSeparatingOn α IsOpen s] : CountablySeparated s :=
  by
  rw [CountablySeparated.subtype_iff]
  exact .mono (fun _ ↦ IsOpen.measurableSet) Subset.rfl

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