Interval

({...} a b) represents the set of natural numbers between a and b. For example, (=_ ({...} (3) (7)) (u. (u. (u. (u. ({} (3)) ({} (4))) ({} (5))) ({} (6))) ({} (7)))). It is defined as (=_ ({...} A B) ({|} x (/\ (<= A x) (<= x B)))) /edit/peano/peano_thms.gh/df-interval.

Theorems

Tuple Overview

Login to edit