Nuprl Lemma : free-vs-subtype

∀[S,T:Type].  ∀[K:CRng]. (Point(free-vs(K;S)) ⊆r Point(free-vs(K;T))) supposing S ⊆r T


Proof

Error : references
Latex:
\mforall{}[S,T:Type].    \mforall{}[K:CRng].  (Point(free-vs(K;S))  \msubseteq{}r  Point(free-vs(K;T)))  supposing  S  \msubseteq{}r  T


Date html generated: 2020_05_21-AM-10_29_12
Last ObjectModification: 2019_08_15-PM-00_50_40

Theory : linear!algebra


Home Index