(*** coafter_sor *)
lemma pr_sor_coafter_dx_tans:
- â\88\80f. ð\9d\90\85â\9dªfâ\9d« â\86\92 â\88\80f2. ð\9d\90\93â\9dªf2â\9d« → ∀f1. f2 ~⊚ f1 ≘ f → ∀f1a,f1b. f1a ⋓ f1b ≘ f1 →
+ â\88\80f. ð\9d\90\85â\9d¨fâ\9d© â\86\92 â\88\80f2. ð\9d\90\93â\9d¨f2â\9d© → ∀f1. f2 ~⊚ f1 ≘ f → ∀f1a,f1b. f1a ⋓ f1b ≘ f1 →
∃∃fa,fb. f2 ~⊚ f1a ≘ fa & f2 ~⊚ f1b ≘ fb & fa ⋓ fb ≘ f.
@pr_isf_ind
[ #f #Hf #f2 #Hf2 #f1 #Hf #f1a #f1b #Hf1
(*** coafter_inv_sor *)
lemma pr_sor_coafter_div:
- â\88\80f. ð\9d\90\85â\9dªfâ\9d« â\86\92 â\88\80f2. ð\9d\90\93â\9dªf2â\9d« → ∀f1. f2 ~⊚ f1 ≘ f → ∀fa,fb. fa ⋓ fb ≘ f →
+ â\88\80f. ð\9d\90\85â\9d¨fâ\9d© â\86\92 â\88\80f2. ð\9d\90\93â\9d¨f2â\9d© → ∀f1. f2 ~⊚ f1 ≘ f → ∀fa,fb. fa ⋓ fb ≘ f →
∃∃f1a,f1b. f2 ~⊚ f1a ≘ fa & f2 ~⊚ f1b ≘ fb & f1a ⋓ f1b ≘ f1.
@pr_isf_ind
[ #f #Hf #f2 #Hf2 #f1 #H1f #fa #fb #H2f