Ico_diff_Ico_left — Mathlib

English

For a linearly ordered set α with locally finite intervals, the left-hand difference of Ico(a,b) by Ico(a,c) is Ico(max(a,c), b).

Русский

При линейном упорядочении α с локально конечными интервалами левая разность между Ico(a,b) и Ico(a,c) равна Ico(max(a,c), b).

LaTeX

$$$Ico(a,b) \\ Ico(a,c) = Ico(\\max(a,c), b)$$$

Lean4

@[simp]
theorem Ico_diff_Ico_left (a b c : α) : Ico a b \ Ico a c = Ico (max a c) b := by
  cases le_total a c with
  | inl h =>
    ext x
    rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, max_eq_right h, and_right_comm, not_and, not_lt]
    exact and_congr_left' ⟨fun hx => hx.2 hx.1, fun hx => ⟨h.trans hx, fun _ => hx⟩⟩
  | inr h => rw [Ico_eq_empty_of_le h, sdiff_empty, max_eq_left h]

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