- function_def
-
|- ∀a b f. function a b f ⇔ ∀x. a x ⇒ b (f x)
- poset_def
-
|- ∀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
- carrier_def
-
|- ∀s r. carrier (s,r) = s
- relation_def
-
|- ∀s r. relation (s,r) = r
- top_def
-
|- ∀s r x. top (s,r) x ⇔ s x ∧ ∀y. s y ⇒ r y x
- bottom_def
-
|- ∀s r x. bottom (s,r) x ⇔ s x ∧ ∀y. s y ⇒ r x y
- chain_def
-
|- ∀s r c. chain (s,r) c ⇔ ∀x y. s x ∧ s y ∧ c x ∧ c y ⇒ r x y ∨ r y x
- lub_def
-
|- ∀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
- glb_def
-
|- ∀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
- complete_def
-
|- ∀p. complete p ⇔ ∀c. (∃x. lub p c x) ∧ ∃x. glb p c x
- pointwise_lift_def
-
|- ∀t s r.
pointwise_lift t (s,r) = (function t s,(λf g. ∀x. t x ⇒ r (f x) (g x)))
- monotonic_def
-
|- ∀s r f. monotonic (s,r) f ⇔ ∀x y. s x ∧ s y ∧ r x y ⇒ r (f x) (f y)
- up_continuous_def
-
|- ∀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)
- down_continuous_def
-
|- ∀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)
- continuous_def
-
|- ∀p f. continuous p f ⇔ up_continuous p f ∧ down_continuous p f
- lfp_def
-
|- ∀s r f x. lfp (s,r) f x ⇔ s x ∧ (f x = x) ∧ ∀y. s y ∧ r (f y) y ⇒ r x y
- gfp_def
-
|- ∀s r f x. gfp (s,r) f x ⇔ s x ∧ (f x = x) ∧ ∀y. s y ∧ r y (f y) ⇒ r y x
- poset_nonempty
-
|- ∀s r. poset (s,r) ⇒ ∃x. s x
- poset_refl
-
|- ∀s r x. poset (s,r) ∧ s x ⇒ r x x
- poset_antisym
-
|- ∀s r x y. poset (s,r) ∧ s x ∧ s y ∧ r x y ∧ r y x ⇒ (x = y)
- poset_trans
-
|- ∀s r x y z. poset (s,r) ∧ s x ∧ s y ∧ s z ∧ r x y ∧ r y z ⇒ r x z
- lub_pred
-
|- ∀s r p x. lub (s,r) (λj. s j ∧ p j) x ⇔ lub (s,r) p x
- glb_pred
-
|- ∀s r p x. glb (s,r) (λj. s j ∧ p j) x ⇔ glb (s,r) p x
- complete_up
-
|- ∀p c. complete p ⇒ ∃x. lub p c x
- complete_down
-
|- ∀p c. complete p ⇒ ∃x. glb p c x
- complete_top
-
|- ∀p. poset p ∧ complete p ⇒ ∃x. top p x
- complete_bottom
-
|- ∀p. poset p ∧ complete p ⇒ ∃x. bottom p x
- complete_pointwise
-
|- ∀p t. complete p ⇒ complete (pointwise_lift t p)
- lfp_unique
-
|- ∀p f x x'. poset p ∧ lfp p f x ∧ lfp p f x' ⇒ (x = x')
- gfp_unique
-
|- ∀p f x x'. poset p ∧ gfp p f x ∧ gfp p f x' ⇒ (x = x')
- knaster_tarski_lfp
-
|- ∀p f.
poset p ∧ complete p ∧ function (carrier p) (carrier p) f ∧
monotonic p f ⇒
∃x. lfp p f x
- knaster_tarski_gfp
-
|- ∀p f.
poset p ∧ complete p ∧ function (carrier p) (carrier p) f ∧
monotonic p f ⇒
∃x. gfp p f x
- knaster_tarski
-
|- ∀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