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

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

Theorems

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
nrange_IN_Uinf 
⊢ {f n | n | T} ≼ 𝕌(:α inf)
increasing 
⊢ ∀f x. strict_mono f ∧ continuous f ⇒ x ≤ f x
clubs_exist 
⊢ strict_mono f ∧ continuous f ⇒ club (IMAGE f 𝕌(:α ordinal))
mono_natI 
⊢ (∀n. f n ≤ f (SUC n)) ⇒ ∀m n. m ≤ n ⇒ f m ≤ f n
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
club_INTER 
⊢ (∀n. club (A n)) ∧ (∀n. A (SUC n) ⊆ A n) ⇒ club (BIGINTER {A n | n | T})