Theory "poset"

Parents pair

Signature

Constant	Type
bottom	:(α -> bool) # (α -> α -> bool) -> α -> bool
carrier	:(α -> bool) # (α -> α -> bool) -> α -> bool
chain	:(α -> bool) # (α -> α -> bool) -> (α -> bool) -> bool
complete	:(α -> bool) # (α -> α -> bool) -> bool
continuous	:(α -> bool) # (α -> α -> bool) -> (α -> α) -> bool
down_continuous	:(α -> bool) # (α -> α -> bool) -> (α -> α) -> bool
function	:(α -> bool) -> (β -> bool) -> (α -> β) -> bool
gfp	:(α -> bool) # (α -> α -> bool) -> (α -> α) -> α -> bool
glb	:(α -> bool) # (α -> α -> bool) -> (α -> bool) -> α -> bool
lfp	:(α -> bool) # (α -> α -> bool) -> (α -> α) -> α -> bool
lub	:(α -> bool) # (α -> α -> bool) -> (α -> bool) -> α -> bool
monotonic	:(α -> bool) # (α -> α -> bool) -> (α -> α) -> bool
pointwise_lift	:(α -> bool) -> (β -> bool) # (β -> β -> bool) -> ((α -> β) -> bool) # ((α -> β) -> (α -> β) -> bool)
poset	:(α -> bool) # (α -> α -> bool) -> bool
relation	:(α -> bool) # (α -> α -> bool) -> α -> α -> bool
top	:(α -> bool) # (α -> α -> bool) -> α -> bool
up_continuous	:(α -> bool) # (α -> α -> bool) -> (α -> α) -> bool

Definitions

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)

top_def

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

relation_def

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

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

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)

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

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

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

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

function_def

⊢ ∀a b f. function a b f ⇔ ∀x. a x ⇒ b (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. p continuous f ⇔ up_continuous p f ∧ down_continuous p f

complete_def

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

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

carrier_def

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

bottom_def

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

Theorems

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

poset_refl

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

poset_nonempty

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

poset_antisym

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

lub_pred

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

lfp_unique

⊢ ∀p f x x'. poset p ∧ lfp p f x ∧ lfp 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

glb_pred

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

gfp_unique

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

complete_up

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

complete_top

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

complete_pointwise

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

complete_down

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

complete_bottom

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