nonempty_Ico_sdiff — Mathlib

English

If dy < dx and 0 < dx in a linearly ordered additive monoid, then the difference of the larger Ico x, x+dx and the smaller Ico y, y+dy is nonempty.

Русский

Если dy < dx и 0 < dx в линейно упорядоченной аддитивной группе, то разность большего Ico x, x+dx и меньшего Ico y, y+dy непустая.

LaTeX

$$$\text{Nonempty} \; \big(Ico(x, x+dx) \setminus Ico(y, y+dy)\big)$$$

Lean4

/-- If we remove a smaller interval from a larger, the result is nonempty -/
theorem nonempty_Ico_sdiff {x dx y dy : α} (h : dy < dx) (hx : 0 < dx) : Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy)) :=
  by
  rcases lt_or_ge x y with h' | h'
  · use x
    simp [*, not_le.2 h']
  · use max x (x + dy)
    simp [*]

Похожие утверждения