The Theory gst-fixp
 Parents
 gst-fun
 Constants
 bnd_mono GS → (GS → GS) → BOOL closed GS → (GS → GS) → BOOL fixed_point GS → (GS → GS) → BOOL least_closed GS → GS → (GS → GS) → BOOL iclosed GS → (GS → GS) → GS lfp GS → (GS → GS) → GS
 Definitions
 bnd_mono ⊢ ∀ D h • bnd_mono D h ⇔ h D ⊆g D ∧ (∀ x y• x ⊆g y ∧ y ⊆g D ⇒ h x ⊆g h y) closed ⊢ ∀ A h• closed A h ⇔ h A ⊆g A fixed_point ⊢ ∀ A h• fixed_point A h ⇔ A = h A least_closed ⊢ ∀ D A h • least_closed D A h ⇔ A ⊆g D ∧ closed A h ∧ (∀ B• B ⊆g D ∧ closed B h ⇒ A ⊆g B) iclosed ⊢ ∀ D h • iclosed D h = ⋂g (Sep (℘g D) (λ X• h X ⊆g X)) lfp ⊢ ∀ D h • bnd_mono D h ⇒ lfp D h ⊆g D ∧ fixed_point (lfp D h) h ∧ least_closed D (lfp D h) h
 Theorems
 bnd_monoI ⊢ ∀ D h • h D ⊆g D ∧ (∀ W X • W ⊆g D ∧ X ⊆g D ∧ W ⊆g X ⇒ h W ⊆g h X) ⇒ bnd_mono D h bnd_monoD1 ⊢ ∀ D h• bnd_mono D h ⇒ h D ⊆g D bnd_monoD2 ⊢ ∀ D h• bnd_mono D h ∧ W ⊆g X ∧ X ⊆g D ⇒ h W ⊆g h X bnd_mono_subset ⊢ ∀ D h• bnd_mono D h ∧ X ⊆g D ⇒ h X ⊆g D bnd_mono_∪g ⊢ ∀ D A B h • bnd_mono D h ∧ A ⊆g D ∧ B ⊆g D ⇒ h A ∪g h B ⊆g h (A ∪g B) def_lfp_subset ⊢ ∀ A D h• A = iclosed D h ⇒ A ⊆g D lfp_greatest ⊢ ∀ A D h • h D ⊆g D ∧ (∀ X• h X ⊆g X ∧ X ⊆g D ⇒ A ⊆g X) ⇒ A ⊆g iclosed D h lfp_lemma1 ⊢ ∀ A D h • bnd_mono D h ∧ h A ⊆g A ∧ A ⊆g D ⇒ h (iclosed D h) ⊆g A lfp_lemma2 ⊢ ∀ A D h • bnd_mono D h ⇒ h (iclosed D h) ⊆g iclosed D h lfp_lemma3 ⊢ ∀ A D h • bnd_mono D h ⇒ iclosed D h ⊆g h (iclosed D h) lfp_Tarski ⊢ ∀ A D h• bnd_mono D h ⇒ iclosed D h = h (iclosed D h) lemp_lemma ⊢ ∀ D h• bnd_mono D h ⇒ least_closed D (iclosed D h) h Tarski_thm ⊢ ∀ D h • bnd_mono D h ⇒ (∃ A • A ⊆g D ∧ fixed_point A h ∧ least_closed D A h) lfp_subset ⊢ ∀ D h• bnd_mono D h ⇒ lfp D h ⊆g D lfp_fixp ⊢ ∀ D h• bnd_mono D h ⇒ h (lfp D h) = lfp D h lfp_lowerbound ⊢ ∀ D h • bnd_mono D h ⇒ (∀ A X• h A ⊆g A ∧ A ⊆g D ⇒ lfp D h ⊆g A) Collect_is_pre_fixedpt ⊢ ∀ D h p • bnd_mono D h ∧ (∀ x• x ∈g h (Sep (lfp D h) p) ⇒ p x) ⇒ closed (Sep (lfp D h) p) h induct ⊢ ∀ D h p a • bnd_mono D h ∧ (∀ x• x ∈g h (Sep (lfp D h) p) ⇒ p x) ∧ a ∈g lfp D h ⇒ p a