---

Step * of Lemma name-morph-satisfies-fl0

∀[I,J:fset(ℕ)]. ∀[i:names(I)]. ∀[f:J ⟶ I].  uiff(((i=0) f) = 1;(f i) = 0 ∈ Point(dM(J)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `name-morph-satisfies` 0
   THEN InstLemma `fl-morph-fl0-is-1` [⌜J⌝;⌜I⌝;⌜f⌝;⌜i⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[i:names(I)].  \mforall{}[f:J  {}\mrightarrow{}  I].    uiff(((i=0)  f)  =  1;(f  i)  =  0)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `name-morph-satisfies`  0
  THEN  InstLemma  `fl-morph-fl0-is-1`  [\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index