Step
*
of Lemma
name-morph-inv_wf
∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  (name-morph-inv(I;f) ∈ name-morph-range(f;I) ⟶ nameset(I))
BY
{ (Auto THEN Unfold `name-morph-inv` 0 THEN (MemCD THENA Auto) THEN RepeatFor 2 (D -1)) }
1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. x : Cname
5. i : nameset(I)
6. (↑isname(f i)) ∧ ((f i) = x ∈ Cname)
⊢ hd(filter(λi.(isname(f i) ∧b (f i =z x));I)) ∈ nameset(I)
Latex:
Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].
    (name-morph-inv(I;f)  \mmember{}  name-morph-range(f;I)  {}\mrightarrow{}  nameset(I))
By
Latex:
(Auto  THEN  Unfold  `name-morph-inv`  0  THEN  (MemCD  THENA  Auto)  THEN  RepeatFor  2  (D  -1))
Home
Index