Nuprl Lemma : function-subtype-top

[A,B:Type].  ((A ⟶ B) ⊆Top)


Proof




Definitions occuring in Statement :  subtype_rel: A ⊆B uall: [x:A]. B[x] top: Top function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B top: Top
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaEquality isect_memberEquality voidElimination voidEquality functionEquality hypothesisEquality sqequalRule axiomEquality because_Cache universeEquality sqequalHypSubstitution isectElimination thin

Latex:
\mforall{}[A,B:Type].    ((A  {}\mrightarrow{}  B)  \msubseteq{}r  Top)



Date html generated: 2016_05_13-PM-04_10_48
Last ObjectModification: 2015_12_26-AM-11_21_50

Theory : subtype_1


Home Index