# Structure veblenTheory

Source File Identifier index Theory binding index

signature veblenTheory =
sig
type thm = Thm.thm

(*  Definitions  *)
val closed_def : thm
val club_def : thm
val continuous_def : thm
val strict_mono_def : thm
val unbounded_def : thm

(*  Theorems  *)
val better_induction : thm
val club_INTER : thm
val clubs_exist : thm
val increasing : thm
val mono_natI : thm
val nrange_IN_Uinf : thm
val oleast_leq : thm
val sup_mem_INTER : thm

val veblen_grammars : type_grammar.grammar * term_grammar.grammar
(*
[ordinal] Parent theory of "veblen"

[closed_def]  Definition

⊢ ∀A. closed A ⇔ ∀g. (∀n. g n ∈ A) ⇒ sup {g n | n | T} ∈ A

[club_def]  Definition

⊢ ∀A. club A ⇔ closed A ∧ unbounded A

[continuous_def]  Definition

⊢ ∀f.
continuous f ⇔
∀A. A ≼ 𝕌(:num + α) ⇒ f (sup A) = sup (IMAGE f A)

[strict_mono_def]  Definition

⊢ ∀f. strict_mono f ⇔ ∀x y. x < y ⇒ f x < f y

[unbounded_def]  Definition

⊢ ∀A. unbounded A ⇔ ∀a. ∃b. b ∈ A ∧ a < b

[better_induction]  Theorem

⊢ ∀P.
P 0 ∧ (∀a. P a ⇒ P a⁺) ∧
(∀a. 0 < a ∧ (∀b. b < a ⇒ P b) ⇒ P (sup (preds a))) ⇒
∀a. P a

[club_INTER]  Theorem

⊢ (∀n. club (A n)) ∧ (∀n. A (SUC n) ⊆ A n) ⇒
club (BIGINTER {A n | n | T})

[clubs_exist]  Theorem

⊢ strict_mono f ∧ continuous f ⇒ club (IMAGE f 𝕌(:α ordinal))

[increasing]  Theorem

⊢ ∀f x. strict_mono f ∧ continuous f ⇒ x ≤ f x

[mono_natI]  Theorem

⊢ (∀n. f n ≤ f (SUC n)) ⇒ ∀m n. m ≤ n ⇒ f m ≤ f n

[nrange_IN_Uinf]  Theorem

⊢ {f n | n | T} ≼ 𝕌(:num + α)

[oleast_leq]  Theorem

⊢ ∀P a. P a ⇒ \$oleast P ≤ a

[sup_mem_INTER]  Theorem

⊢ (∀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}

*)
end

Source File Identifier index Theory binding index