English
Measurable sets can be constructed from open sets using complementation and countable disjoint unions, via an induction principle.
Русский
Измеримые множества можно получать из открытых через дополнение и счётные попарно непересекающиеся объединения, по принципу индукции.
LaTeX
$$$$ \forall C : (\mathcal{P}(\gamma) \to \text{MeasurableSet}\,\cdot) \,\Big(\forall U\, (hU : IsOpen U), C(U) \Big) \\ \land \\ \forall t\,(ht : \text{MeasurableSet } t), C(t) \Rightarrow C(t^{c}) \land \\ \text{(iUnion condition with disjoint f)} \Rightarrow \forall t\, (ht : \text{MeasurableSet } t), C(t). $$$$
Lean4
@[elab_as_elim]
theorem induction_on_open {C : ∀ s : Set γ, MeasurableSet s → Prop} (isOpen : ∀ U (hU : IsOpen U), C U hU.measurableSet)
(compl : ∀ t (ht : MeasurableSet t), C t ht → C tᶜ ht.compl)
(iUnion :
∀ f : ℕ → Set γ,
Pairwise (Disjoint on f) →
∀ (hf : ∀ i, MeasurableSet (f i)), (∀ i, C (f i) (hf i)) → C (⋃ i, f i) (.iUnion hf)) :
∀ t (ht : MeasurableSet t), C t ht := fun t ht ↦
MeasurableSpace.induction_on_inter BorelSpace.measurable_eq isPiSystem_isOpen (isOpen _ isOpen_empty) isOpen compl
iUnion t ht
