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` THEN (MemCD THENA Auto) THEN RepeatFor (D -1)) }

1
1. Cname List
2. Cname List
3. name-morph(I;J)
4. Cname
5. nameset(I)
6. (↑isname(f i)) ∧ ((f i) x ∈ Cname)
⊢ hd(filter(λi.(isname(f i) ∧b (f =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