Theory "tightness"

Parents     indexedLists   patternMatches

Signature

Constant Type
tight_bound :(α -> num) -> (α -> β -> bool) -> (β -> num) -> bool
valid_bound :(α -> num) -> (α -> β -> bool) -> (β -> num) -> bool

Definitions

valid_bound_def
|- ∀f R g. valid_bound f R g ⇔ ∀x y. R x y ⇒ f x ≤ g y
tight_bound_def
|- ∀f R g.
     tight_bound f R g ⇔
     valid_bound f R g ∧ ∀y. (∃x. R x y) ⇒ ∃x'. R x' y ∧ (f x' = g y)


Theorems

tight_works
|- tight_bound f R g ∧ h y < g y ∧ (∃x. R x y) ⇒ ¬valid_bound f R h
valid_compose
|- valid_bound f R (g ∘ h) ⇔ valid_bound f (λx y. ∃z. R x z ∧ (h z = y)) g
tight_compose_1
|- SURJ h 𝕌(:α) 𝕌(:β) ⇒
   tight_bound f R (g ∘ h) ⇒
   tight_bound f (λx y. ∃z. R x z ∧ (h z = y)) g
tight_compose_2
|- INJ h 𝕌(:α) 𝕌(:β) ⇒
   tight_bound f (λx y. ∃z. R x z ∧ (h z = y)) g ⇒
   tight_bound f R (g ∘ h)
tight_same_dom
|- tight_bound f R g ∧ (∀x y. R x y ⇒ (x = fst y)) ⇒ ∀x. R x y ⇒ (f x = g y)
tight_compose_1_cor
|- SURJ h 𝕌(:α) 𝕌(:β) ⇒
   tight_bound f R (g ∘ h) ⇒
   tight_bound (g ∘ h) (λx y. h x = y) g
tight_compose_2_cor
|- INJ h 𝕌(:α) 𝕌(:β) ⇒
   tight_bound f (λx y. ∃z. R x z ∧ (h z = y)) g ⇒
   tight_bound g (λx y. h y = x) (g ∘ h)