Theory fixedPoint

⊢ ∀f X. closed f X ⇔ f X ⊆ X

⊢ ∀f X. dense f X ⇔ X ⊆ f X

⊢ empty = (λX. ∅)

⊢ ∀f1 f2 X. fnsum f1 f2 X = f1 X ∪ f2 X

⊢ ∀f. gfp f = BIGUNION {X | X ⊆ f X}

⊢ ∀f. lfp f = BIGINTER {X | f X ⊆ X}

⊢ ∀f. monotone f ⇔ ∀X Y. X ⊆ Y ⇒ f X ⊆ f Y

⊢ complete (𝕌(:α -> bool),$SUBSET)

⊢ poset (𝕌(:α -> bool),$SUBSET)

⊢ monotone empty

⊢ ∀f g h. fnsum f (fnsum g h) = fnsum (fnsum f g) h

⊢ ∀f g. fnsum f g = fnsum g f

⊢ ∀f g X. f X ⊆ fnsum f g X ∧ g X ⊆ fnsum f g X

⊢ ∀f. fnsum f empty = f ∧ fnsum empty f = f

⊢ ∀f1 f2. monotone f1 ∧ monotone f2 ⇒ monotone (fnsum f1 f2)

⊢ ∀f. monotone f ⇒ ∀X. X ⊆ f X ⇒ X ⊆ gfp f

⊢ ∀f. monotone f ⇒ dense f (gfp f) ∧ ∀X. dense f X ⇒ X ⊆ gfp f

⊢ ∀f. monotone f ⇒ f (gfp f) = gfp f ∧ ∀X. f X = X ⇒ X ⊆ gfp f

⊢ monotone f ⇒ po_gfp (𝕌(:α -> bool),$SUBSET) f (gfp f)

⊢ ∀f. monotone f ⇒ ∀X. X ⊆ f (X ∪ gfp f) ⇒ X ⊆ gfp f

⊢ ∀f x. monotone f ∧ x ∈ f ∅ ⇒ x ∈ lfp f

⊢ ∀f. monotone f ⇒ f (lfp f) = lfp f ∧ ∀X. f X = X ⇒ lfp f ⊆ X

⊢ ∀f1 f2.
    monotone f1 ∧ monotone f2 ⇒
    lfp f1 ⊆ lfp (fnsum f1 f2) ∧ lfp f2 ⊆ lfp (fnsum f1 f2)

⊢ ∀f. monotone f ⇒ ∀X. f X ⊆ X ⇒ lfp f ⊆ X

⊢ ∀f. monotone f ⇒ closed f (lfp f) ∧ ∀X. closed f X ⇒ lfp f ⊆ X

⊢ monotone f ⇒ po_lfp (𝕌(:α -> bool),$SUBSET) f (lfp f)

⊢ ∀f X y. monotone f ∧ X ⊆ lfp f ∧ y ∈ f X ⇒ y ∈ lfp f

⊢ ∀f. monotone f ⇒ ∀X. f (X ∩ lfp f) ⊆ X ⇒ lfp f ⊆ X

⊢ monotonic (𝕌(:α -> bool),$SUBSET) f ⇔ monotone f