2023-04-18 17:29:19 +00:00
|
|
|
import Mathlib.Data.Real.Basic
|
|
|
|
|
|
2023-05-04 22:37:54 +00:00
|
|
|
/-! # Bookshelf.Real.Set.Interval
|
|
|
|
|
|
|
|
|
|
A syntactic description of the various types of continuous intervals permitted
|
|
|
|
|
on the real number line.
|
|
|
|
|
-/
|
|
|
|
|
|
2023-04-18 17:29:19 +00:00
|
|
|
/--
|
|
|
|
|
Representation of a closed interval.
|
|
|
|
|
-/
|
|
|
|
|
syntax (priority := high) "i[" term "," term "]" : term
|
|
|
|
|
|
|
|
|
|
macro_rules
|
|
|
|
|
| `(i[$a, $b]) => `({ z | $a ≤ z ∧ z ≤ $b })
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
Representation of an open interval.
|
|
|
|
|
-/
|
|
|
|
|
syntax (priority := high) "i(" term "," term ")" : term
|
|
|
|
|
|
|
|
|
|
macro_rules
|
|
|
|
|
| `(i($a, $b)) => `({ z | $a < z ∧ z < $b })
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
Representation of a left half-open interval.
|
|
|
|
|
-/
|
|
|
|
|
syntax (priority := high) "i(" term "," term "]" : term
|
|
|
|
|
|
|
|
|
|
macro_rules
|
|
|
|
|
| `(i($a, $b]) => `({ z | $a < z ∧ z ≤ $b })
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
Representation of a right half-open interval.
|
|
|
|
|
-/
|
|
|
|
|
syntax (priority := high) "i[" term "," term ")" : term
|
|
|
|
|
|
|
|
|
|
macro_rules
|
|
|
|
|
| `(i[$a, $b)) => `({ z | $a ≤ z ∧ z < $b })
|
