Ici_erase — Mathlib

English

In a locally finite order with top element, erasing the left endpoint a from Ici(a) yields the strictly greater elements Ioi(a).

Русский

В локально конечном порядке с верхней границей удаление левой границы a из Ici(a) даёт множества элементов строго больше a: Ioi(a).

LaTeX

$$$$ (Ici(a)).erase(a) = Ioi(a) $$$$

Lean4

@[simp]
theorem Ici_erase [DecidableEq α] (a : α) : (Ici a).erase a = Ioi a :=
  by
  ext
  simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]

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