`Interval`

definition

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.Basic
domain: Numerics
line: 16 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Numerics.Interval.Basic on GitHub at line 16.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  13namespace IndisputableMonolith.Numerics
  14
  15/-- A closed interval with rational endpoints. -/
  16structure Interval where
  17  lo : ℚ
  18  hi : ℚ
  19  valid : lo ≤ hi
  20  deriving DecidableEq
  21
  22namespace Interval
  23
  24/-- Containment: a real number x is in interval I if lo ≤ x ≤ hi -/
  25def contains (I : Interval) (x : ℝ) : Prop :=
  26  (I.lo : ℝ) ≤ x ∧ x ≤ (I.hi : ℝ)
  27
  28/-- Point interval containing a single rational -/
  29def point (q : ℚ) : Interval where
  30  lo := q
  31  hi := q
  32  valid := le_refl q
  33
  34theorem contains_point (q : ℚ) : (point q).contains (q : ℝ) :=
  35  ⟨le_refl _, le_refl _⟩
  36
  37/-- Interval from explicit bounds -/
  38def mk' (lo hi : ℚ) (h : lo ≤ hi := by decide) : Interval where
  39  lo := lo
  40  hi := hi
  41  valid := h
  42
  43/-! ## Interval Arithmetic Operations -/
  44
  45/-- Addition of intervals: [a,b] + [c,d] = [a+c, b+d] -/
  46def add (I J : Interval) : Interval where

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.