Theory poset

⊢ ∀s r x. bottom (s,r) x ⇔ s x ∧ ∀y. s y ⇒ r x y

⊢ ∀s r. carrier (s,r) = s

⊢ ∀s r c. chain (s,r) c ⇔ ∀x y. s x ∧ s y ∧ c x ∧ c y ⇒ r x y ∨ r y x

⊢ ∀p. complete p ⇔ ∀c. (∃x. lub p c x) ∧ ∃x. glb p c x

⊢ ∀p f. continuous p f ⇔ up_continuous p f ∧ down_continuous p f

⊢ ∀s r f.
    down_continuous (s,r) f ⇔
    ∀c x.
      chain (s,r) c ∧ glb (s,r) c x ⇒
      glb (s,r) (λy. ∃z. (s z ∧ c z) ∧ y = f z) (f x)

⊢ ∀a b f. function a b f ⇔ ∀x. a x ⇒ b (f x)

⊢ ∀s r f x. gfp (s,r) f x ⇔ s x ∧ f x = x ∧ ∀y. s y ∧ r y (f y) ⇒ r y x

⊢ ∀s r p x.
    glb (s,r) p x ⇔
    s x ∧ (∀y. s y ∧ p y ⇒ r x y) ∧
    ∀z. s z ∧ (∀y. s y ∧ p y ⇒ r z y) ⇒ r z x

⊢ ∀s r f x. lfp (s,r) f x ⇔ s x ∧ f x = x ∧ ∀y. s y ∧ r (f y) y ⇒ r x y

⊢ ∀s r p x.
    lub (s,r) p x ⇔
    s x ∧ (∀y. s y ∧ p y ⇒ r y x) ∧
    ∀z. s z ∧ (∀y. s y ∧ p y ⇒ r y z) ⇒ r x z

⊢ ∀s r f. monotonic (s,r) f ⇔ ∀x y. s x ∧ s y ∧ r x y ⇒ r (f x) (f y)

⊢ ∀t s r.
    pointwise_lift t (s,r) = (function t s,(λf g. ∀x. t x ⇒ r (f x) (g x)))

⊢ ∀s r.
    poset (s,r) ⇔
    (∃x. s x) ∧ (∀x. s x ⇒ r x x) ∧
    (∀x y. s x ∧ s y ∧ r x y ∧ r y x ⇒ x = y) ∧
    ∀x y z. s x ∧ s y ∧ s z ∧ r x y ∧ r y z ⇒ r x z

⊢ ∀s r. relation (s,r) = r

⊢ ∀s r x. top (s,r) x ⇔ s x ∧ ∀y. s y ⇒ r y x

⊢ ∀s r f.
    up_continuous (s,r) f ⇔
    ∀c x.
      chain (s,r) c ∧ lub (s,r) c x ⇒
      lub (s,r) (λy. ∃z. (s z ∧ c z) ∧ y = f z) (f x)

⊢ ∀p. poset p ∧ complete p ⇒ ∃x. bottom p x

⊢ ∀p c. complete p ⇒ ∃x. glb p c x

⊢ ∀p t. complete p ⇒ complete (pointwise_lift t p)

⊢ ∀p. poset p ∧ complete p ⇒ ∃x. top p x

⊢ ∀p c. complete p ⇒ ∃x. lub p c x

⊢ function s s t ∧ s x ⇒ s (t x)

⊢ gfp (s,r) b gfix ∧ s x ∧ r x (b x) ⇒ r x gfix

⊢ ∀p f x x'. poset p ∧ gfp p f x ∧ gfp p f x' ⇒ x = x'

⊢ ∀s r p x. glb (s,r) (λj. s j ∧ p j) x ⇔ glb (s,r) p x

⊢ poset (s,r) ∧ glb (s,r) P x ∧ glb (s,r) P y ⇒ x = y

⊢ ∀p f.
    poset p ∧ complete p ∧ function (carrier p) (carrier p) f ∧
    monotonic p f ⇒
    (∃x. lfp p f x) ∧ ∃x. gfp p f x

⊢ ∀p f.
    poset p ∧ complete p ∧ function (carrier p) (carrier p) f ∧
    monotonic p f ⇒
    ∃x. gfp p f x

⊢ ∀p f.
    poset p ∧ complete p ∧ function (carrier p) (carrier p) f ∧
    monotonic p f ⇒
    ∃x. lfp p f x

⊢ lfp (s,r) b lfix ∧ s x ∧ r (b x) x ⇒ r lfix x

⊢ ∀p f x x'. poset p ∧ lfp p f x ∧ lfp p f x' ⇒ x = x'

⊢ ∀s r p x. lub (s,r) (λj. s j ∧ p j) x ⇔ lub (s,r) p x

⊢ poset (s,r) ∧ lub (s,r) P x ∧ lub (s,r) P y ⇒ x = y

⊢ monotonic (s,r) f ∧ monotonic (s,r) g ∧ function s s g ⇒
  monotonic (s,r) (f ∘ g)

⊢ ∀s r x y. poset (s,r) ∧ s x ∧ s y ∧ r x y ∧ r y x ⇒ x = y

⊢ ∀s r. poset (s,r) ⇒ ∃x. s x

⊢ ∀s r x. poset (s,r) ∧ s x ⇒ r x x

⊢ ∀s r x y z. poset (s,r) ∧ s x ∧ s y ∧ s z ∧ r x y ∧ r y z ⇒ r x z