`contains`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  47  lo := I.lo + J.lo
  48  hi := I.hi + J.hi
  49  valid := add_le_add I.valid J.valid
  50
  51instance : Add Interval where
  52  add := add
  53
  54@[simp] theorem add_lo (I J : Interval) : (I + J).lo = I.lo + J.lo := rfl
  55@[simp] theorem add_hi (I J : Interval) : (I + J).hi = I.hi + J.hi := rfl

papers checked against this theorem

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