pith. machine review for the scientific record. sign in
theorem proved term proof

sub_contains_sub

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  96theorem sub_contains_sub {x y : ℝ} {I J : Interval}
  97    (hx : I.contains x) (hy : J.contains y) : (I - J).contains (x - y) := by

proof body

Term-mode proof.

  98  constructor
  99  · simp only [sub_lo, Rat.cast_sub]
 100    exact sub_le_sub hx.1 hy.2
 101  · simp only [sub_hi, Rat.cast_sub]
 102    exact sub_le_sub hx.2 hy.1
 103
 104/-- Multiplication for positive intervals -/

depends on (7)

Lean names referenced from this declaration's body.