Nuprl Definition : subtype_rel
A ⊆r B == λx.x ∈ A ⟶ B
Definitions occuring in Statement :
member: t ∈ T,
lambda: λx.A[x],
function: x:A ⟶ B[x]
Definitions occuring in definition :
member: t ∈ T,
function: x:A ⟶ B[x],
lambda: λx.A[x]
Rules referencing :
StrongContinuity2,
hypothesis_subsumption
FDL editor aliases :
subtyperel
Latex:
A \msubseteq{}r B == \mlambda{}x.x \mmember{} A {}\mrightarrow{} B
Date html generated:
2016_05_13-PM-03_06_46
Last ObjectModification:
2015_09_22-PM-05_43_46
Theory : core_2
Home
Index