English
An induction principle for the elements of generateMeasurableRec: if p holds for basic steps and is preserved under complement and countable unions, then p holds for all elements at stage i.
Русский
Индуктивный принцип для элементов generateMeasurableRec: если p истинно для базовых этапов и сохраняется при дополнении и счетных объединениях, то p истинно на стадии i.
LaTeX
$$$\\text{generateMeasurableRec\_induction} \\; (s,i,p) \\;:\\; (\\text{basis and closure conditions}) \\Rightarrow (t \\in \\mathrm{generateMeasurableRec}(s,i) \\Rightarrow p(t))$$$
Lean4
/-- An inductive principle for the elements of `generateMeasurableRec`. -/
@[elab_as_elim]
theorem generateMeasurableRec_induction {s : Set (Set α)} {i : Ordinal} {t : Set α} {p : Set α → Prop}
(hs : ∀ t ∈ s, p t) (h0 : p ∅) (hc : ∀ u, p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ)
(hn : ∀ f : ℕ → Set α, (∀ n, p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)) :
t ∈ generateMeasurableRec s i → p t :=
by
suffices H : ∀ k ≤ i, ∀ t ∈ generateMeasurableRec s k, p t from H i le_rfl t
intro k
apply WellFoundedLT.induction k
intro k IH hk t
replace IH := fun j hj => IH j hj (hj.le.trans hk)
unfold generateMeasurableRec
rintro (((ht | rfl) | ht) | ⟨f, rfl⟩)
· exact hs t ht
· exact h0
· simp_rw [mem_image, mem_iUnion₂] at ht
obtain ⟨u, ⟨⟨j, hj, hj'⟩, rfl⟩⟩ := ht
exact hc u (IH j hj u hj') ⟨j, hj.trans_le hk, hj'⟩
· apply hn
intro n
obtain ⟨j, hj, hj'⟩ := mem_iUnion₂.1 (f n).2
use IH j hj _ hj', j, hj.trans_le hk
