Nuprl Definition : is-above
is-above(T;a;z) == ∃y:Base. ((y = a ∈ T) ∧ (y ≤ z))
Definitions occuring in Statement :
exists: ∃x:A. B[x],
and: P ∧ Q,
base: Base,
sqle: s ≤ t,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
base: Base,
and: P ∧ Q,
equal: s = t ∈ T,
sqle: s ≤ t
FDL editor aliases :
is-above
Latex:
is-above(T;a;z) == \mexists{}y:Base. ((y = a) \mwedge{} (y \mleq{} z))
Date html generated:
2016_05_13-PM-04_12_58
Last ObjectModification:
2015_09_22-PM-05_45_58
Theory : subtype_1
Home
Index