- 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)