(*** isfin *)
definition pr_isf: predicate pr_map ≝
- λf. â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n.
+ λf. â\88\83n. ð\9d\90\82â\9d¨fâ\9d© ≘ n.
interpretation
"finite colength condition (partial relocation maps)"
(*** isfin_ind *)
lemma pr_isf_ind (Q:predicate …):
- (â\88\80f. ð\9d\90\88â\9dªfâ\9d« → Q f) →
- (â\88\80f. ð\9d\90\85â\9dªfâ\9d« → Q f → Q (⫯f)) →
- (â\88\80f. ð\9d\90\85â\9dªfâ\9d« → Q f → Q (↑f)) →
- â\88\80f. ð\9d\90\85â\9dªfâ\9d« → Q f.
+ (â\88\80f. ð\9d\90\88â\9d¨fâ\9d© → Q f) →
+ (â\88\80f. ð\9d\90\85â\9d¨fâ\9d© → Q f → Q (⫯f)) →
+ (â\88\80f. ð\9d\90\85â\9d¨fâ\9d© → Q f → Q (↑f)) →
+ â\88\80f. ð\9d\90\85â\9d¨fâ\9d© → Q f.
#Q #IH1 #IH2 #IH3 #f #H elim H -H
#n #H elim H -f -n /3 width=2 by ex_intro/
qed-.
(* Basic inversions *********************************************************)
(*** isfin_inv_push *)
-lemma pr_isf_inv_push (g): ð\9d\90\85â\9dªgâ\9d« â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+lemma pr_isf_inv_push (g): ð\9d\90\85â\9d¨gâ\9d© â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
#g * /3 width=4 by pr_fcla_inv_push, ex_intro/
qed-.
(*** isfin_inv_next *)
-lemma pr_isf_inv_next (g): ð\9d\90\85â\9dªgâ\9d« â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+lemma pr_isf_inv_next (g): ð\9d\90\85â\9d¨gâ\9d© â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
#g * #n #H #f #H0 elim (pr_fcla_inv_next … H … H0) -g
/2 width=2 by ex_intro/
qed-.
(* Basic constructions ******************************************************)
(*** isfin_isid *)
-lemma pr_isf_isi (f): ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+lemma pr_isf_isi (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
/3 width=2 by pr_fcla_isi, ex_intro/ qed.
(*** isfin_push *)
-lemma pr_isf_push (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ«¯fâ\9d«.
+lemma pr_isf_push (f): ð\9d\90\85â\9d¨fâ\9d© â\86\92 ð\9d\90\85â\9d¨â«¯fâ\9d©.
#f * /3 width=2 by pr_fcla_push, ex_intro/
qed.
(*** isfin_next *)
-lemma pr_isf_next (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ\86\91fâ\9d«.
+lemma pr_isf_next (f): ð\9d\90\85â\9d¨fâ\9d© â\86\92 ð\9d\90\85â\9d¨â\86\91fâ\9d©.
#f * /3 width=2 by pr_fcla_next, ex_intro/
qed.