Ico_diff_Ico_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ico_diff_Ico_right (a b c : α) : Ico a b \ Ico c b = Ico a (min b c) := by
  cases le_total b c with
  | inl h => rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
  | inr h =>
    ext x
    rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
    exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩

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