Theory veblen

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

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

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

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

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

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

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

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

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

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

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

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

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