α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ a < ord c → derivFamily f a < ord c
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
⊢ a < ord c → derivFamily f a < ord c
have hω : ℵ₀ < c.ord.cof := by
  rw [hc.cof_eq]
  exact lt_of_le_of_ne hc.1 hc'.symm
case H₁
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ 0 < ord c → derivFamily f 0 < ord c

case H₂
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ ∀ (o : Ordinal), (o < ord c → derivFamily f o < ord c) → succ o < ord c → derivFamily f (succ o) < ord c

case H₃
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ ∀ (o : Ordinal),
    Ordinal.IsLimit o →
      (∀ (o' : Ordinal), o' < o → o' < ord c → derivFamily f o' < ord c) → o < ord c → derivFamily f o < ord c
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ a < ord c → derivFamily f a < ord c
apply a.limitRecOn
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
⊢ ℵ₀ < c
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
⊢ ℵ₀ < Ordinal.cof (ord c)
rw [hc.cof_eq]
no goals
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
⊢ ℵ₀ < c
exact lt_of_le_of_ne hc.1 hc'.symm
case H₁
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ 0 < ord c → nfpFamily f 0 < ord c
case H₁
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ 0 < ord c → derivFamily f 0 < ord c
rw [derivFamily_zero]
no goals
case H₁
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ 0 < ord c → nfpFamily f 0 < ord c
exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf
no goals
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ lift (#ι) < Ordinal.cof (ord c)
rwa [hc.cof_eq]
case H₂
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
b : Ordinal
hb : b < ord c → derivFamily f b < ord c
hb' : succ b < ord c
⊢ derivFamily f (succ b) < ord c
case H₂
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ ∀ (o : Ordinal), (o < ord c → derivFamily f o < ord c) → succ o < ord c → derivFamily f (succ o) < ord c
intro b hb hb'
case H₂
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
b : Ordinal
hb : b < ord c → derivFamily f b < ord c
hb' : succ b < ord c
⊢ nfpFamily f (succ (derivFamily f b)) < ord c
case H₂
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
b : Ordinal
hb : b < ord c → derivFamily f b < ord c
hb' : succ b < ord c
⊢ derivFamily f (succ b) < ord c
rw [derivFamily_succ]
no goals
case H₂
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
b : Ordinal
hb : b < ord c → derivFamily f b < ord c
hb' : succ b < ord c
⊢ nfpFamily f (succ (derivFamily f b)) < ord c
exact
  nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf
    ((ord_isLimit hc.1).2 _ (hb ((lt_succ b).trans hb')))
no goals
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
b : Ordinal
hb : b < ord c → derivFamily f b < ord c
hb' : succ b < ord c
⊢ lift (#ι) < Ordinal.cof (ord c)
rwa [hc.cof_eq]
case H₃
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
b : Ordinal
hb : Ordinal.IsLimit b
H : ∀ (o' : Ordinal), o' < b → o' < ord c → derivFamily f o' < ord c
hb' : b < ord c
⊢ derivFamily f b < ord c
case H₃
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
⊢ ∀ (o : Ordinal),
    Ordinal.IsLimit o →
      (∀ (o' : Ordinal), o' < o → o' < ord c → derivFamily f o' < ord c) → o < ord c → derivFamily f o < ord c
intro b hb H hb'
case H₃
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
b : Ordinal
hb : Ordinal.IsLimit b
H : ∀ (o' : Ordinal), o' < b → o' < ord c → derivFamily f o' < ord c
hb' : b < ord c
⊢ (bsup b fun a x => derivFamily f a) < ord c
case H₃
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
b : Ordinal
hb : Ordinal.IsLimit b
H : ∀ (o' : Ordinal), o' < b → o' < ord c → derivFamily f o' < ord c
hb' : b < ord c
⊢ derivFamily f b < ord c
rw [derivFamily_limit f hb]
no goals
case H₃
α : Type ?u.164801
r : α → α → Prop
ι : Type u
f : ι → Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hι : lift (#ι) < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι) (b : Ordinal), b < ord c → f i b < ord c
a : Ordinal
hω : ℵ₀ < Ordinal.cof (ord c)
b : Ordinal
hb : Ordinal.IsLimit b
H : ∀ (o' : Ordinal), o' < b → o' < ord c → derivFamily f o' < ord c
hb' : b < ord c
⊢ (bsup b fun a x => derivFamily f a) < ord c
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')