Nuprl Lemma : subtype-set
(T:Type × (T ⟶ Set{i:l})) ⊆r Set{i:l}
Proof
Definitions occuring in Statement :
Set: Set{i:l},
subtype_rel: A ⊆r B,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
ext-eq: A ≡ B,
and: P ∧ Q
Lemmas referenced :
set-ext
Rules used in proof :
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
productElimination,
thin
Latex:
(T:Type \mtimes{} (T {}\mrightarrow{} Set\{i:l\})) \msubseteq{}r Set\{i:l\}
Date html generated:
2018_05_22-PM-09_47_37
Last ObjectModification:
2018_05_16-PM-01_31_07
Theory : constructive!set!theory
Home
Index