---

Step * of Lemma fpf-dom-type

∀[X,Y:Type]. ∀[eq:EqDecider(Y)]. ∀[f:x:X fp-> Top]. ∀[x:Y].  (x ∈ X) supposing ((↑x ∈ dom(f)) and strong-subtype(X;Y))
BY
{ (Auto 
   THEN (Using [`L',⌈fpf-domain(f)⌉] (BLemma `strong-subtype-l_member-type`))⋅
   THEN Auto
   THEN RWO "member-fpf-domain" (-1)
   THEN Auto) }

---

Latex:


\mforall{}[X,Y:Type].  \mforall{}[eq:EqDecider(Y)].  \mforall{}[f:x:X  fp->  Top].  \mforall{}[x:Y].
    (x  \mmember{}  X)  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  strong-subtype(X;Y))


By

(Auto 
  THEN  (Using  [`L',\mkleeneopen{}fpf-domain(f)\mkleeneclose{}]  (BLemma  `strong-subtype-l\_member-type`))\mcdot{}
  THEN  Auto
  THEN  RWO  "member-fpf-domain"  (-1)
  THEN  Auto)

---

Home Index