derivFamily_lt_ord_lift — Mathlib

English

Let hc be IsRegular c and hι lift(#ι) < c. If hf ensures f i b < c.ord for all i and b < c.ord, then for all a < c.ord, derivFamily f a < c.ord.

Русский

Пусть c регулярное, hι: lift(#ι) < c. Тогда если hf обеспечивает f i b < c.ord для всех i и b < c.ord, то для каждого a < c.ord, derivFamily f a < c.ord.

LaTeX

$$$IsRegular(c) \land \operatorname{lift}(\#ι) < c \Rightarrow ( \forall i, \forall b < \operatorname{ord}(c),\ f(i,b) < \operatorname{ord}(c) ) \Rightarrow \forall a < \operatorname{ord}(c),\operatorname{derivFamily}(f,a) < \operatorname{ord}(c)$$$

Lean4

theorem derivFamily_lt_ord_lift {ι : Type u} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c) (hι : lift.{v} #ι < c)
    (hc' : c ≠ ℵ₀) (hf : ∀ i, ∀ b < c.ord, f i b < c.ord) {a} : a < c.ord → derivFamily f a < c.ord :=
  by
  have hω : ℵ₀ < c.ord.cof := by
    rw [hc.cof_eq]
    exact lt_of_le_of_ne hc.1 hc'.symm
  induction a using limitRecOn with
  | zero =>
    rw [derivFamily_zero]
    exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf
  | succ b hb =>
    intro hb'
    rw [derivFamily_succ]
    exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf ((isSuccLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))
  | limit b hb H =>
    intro hb'
    have : ⨆ a : Iio b, _ = _ := iSup_Iio_eq_bsup (f := fun x (_ : x < b) ↦ derivFamily f x)
    rw [derivFamily_limit f hb, this]
    exact
      bsup_lt_ord_of_isRegular.{u, v} hc (ord_lt_ord.1 ((ord_card_le b).trans_lt hb')) fun o' ho' =>
        H o' ho' (ho'.trans hb')

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