Nuprl Definition : less_than

At one time, ⌜a < b⌝ was 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 < ==  ↓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

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