Theory "veblen"

Parents     ordinal

Signature

Constant Type
closed :(α ordinal -> bool) -> bool
club :(α ordinal -> bool) -> bool
continuous :(α ordinal -> β ordinal) -> bool
strict_mono :(α ordinal -> β ordinal) -> bool
unbounded :(α ordinal -> bool) -> bool

Definitions

unbounded_def 
⊢ ∀A. unbounded A ⇔ ∀a. ∃b. b ∈ A ∧ a < b
strict_mono_def 
⊢ ∀f. strict_mono f ⇔ ∀x y. x < y ⇒ f x < f y
continuous_def 
⊢ ∀f. $continuous f ⇔ ∀A. A ≼ 𝕌(:num + α) ⇒ (f (sup A) = sup (IMAGE f A))
club_def 
⊢ ∀A. club A ⇔ closed A ∧ unbounded A
closed_def 
⊢ ∀A. closed A ⇔ ∀g. (∀n. g n ∈ A) ⇒ sup {g n | n | T} ∈ A

Theorems

sup_mem_INTER 
⊢ (∀n. club (A n)) ∧ (∀n. A (SUC n) ⊆ A n) ∧ (∀n. f n ∈ A n) ∧
  (∀m n. m ≤ n ⇒ f m ≤ f n) ⇒
  sup {f n | n | T} ∈ BIGINTER {A n | n | T}
oleast_leq 
⊢ ∀P a. P a ⇒ $oleast P ≤ a
nrange_IN_Uinf 
⊢ {f n | n | T} ≼ 𝕌(:num + α)
mono_natI 
⊢ (∀n. f n ≤ f (SUC n)) ⇒ ∀m n. m ≤ n ⇒ f m ≤ f n
increasing 
⊢ ∀f x. strict_mono f ∧ $continuous f ⇒ x ≤ f x
clubs_exist 
⊢ strict_mono f ∧ $continuous f ⇒ club (IMAGE f 𝕌(:α ordinal))
club_INTER 
⊢ (∀n. club (A n)) ∧ (∀n. A (SUC n) ⊆ A n) ⇒ club (BIGINTER {A n | n | T})
better_induction 
⊢ ∀P.
      P 0 ∧ (∀a. P a ⇒ P a⁺) ∧
      (∀a. 0 < a ∧ (∀b. b < a ⇒ P b) ⇒ P (sup (preds a))) ⇒
      ∀a. P a