Nuprl Definition : less_than
At one time, ⌜a < b⌝ was a primitive type but the properties we need all
follow from the definition of ⌜less_than'(a;b)⌝ except for the
property that from ⌜a < b⌝ we can derive ⌜(a ∈ ℤ) ∧ (b ∈ ℤ)⌝.
So we simply add those to the definition..
⋅
a < b == ↓less_than'(a;b) ∧ (a ∈ ℤ) ∧ (b ∈ ℤ)
Definitions occuring in Statement :
less_than': less_than'(a;b),
squash: ↓T,
and: P ∧ Q,
member: t ∈ T,
int: ℤ
Definitions occuring in definition :
squash: ↓T,
less_than': less_than'(a;b),
and: P ∧ Q,
member: t ∈ T,
int: ℤ
Rules referencing :
addMonotonic,
lessDiscrete,
lessTrichotomy,
multiplyPositive,
remainderBounds1,
remainderBounds3,
remainderBounds4,
intWeakElimination,
lessEquality,
Continuity
FDL editor aliases :
lt
Latex:
a < b == \mdownarrow{}less\_than'(a;b) \mwedge{} (a \mmember{} \mBbbZ{}) \mwedge{} (b \mmember{} \mBbbZ{})
Date html generated:
2016_07_08-PM-04_46_41
Last ObjectModification:
2015_09_22-PM-05_44_27
Theory : core_2
Home
Index