|
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
|
