generateMeasurableRec_of_omega1_le

English

For any s and any i with ω1 ≤ i, the i-th stage of the transfinite generation equals the ω1-th stage: generateMeasurableRec(s,i) = generateMeasurableRec(s, ω1).

Русский

Для любого s и любого i с ω1 ≤ i тождественна стадия i порождения: generateMeasurableRec(s,i) = generateMeasurableRec(s, ω1).

LaTeX

$$$\\text{generateMeasurableRec}(s,i) = \\text{generateMeasurableRec}(s, \\omega_1) \\quad\\text{whenever } \\omega_1 \\le i$$$

Lean4

/-- `generateMeasurableRec` is constant for ordinals `≥ ω₁`. -/
theorem generateMeasurableRec_of_omega1_le (s : Set (Set α)) {i : Ordinal.{v}} (hi : ω₁ ≤ i) :
    generateMeasurableRec s i = generateMeasurableRec s (ω₁ : Ordinal.{v}) :=
  by
  apply (generateMeasurableRec_mono s hi).antisymm'
  rw [← generateMeasurable_eq_rec]
  exact generateMeasurableRec_subset s i

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