Ioi_insert — Mathlib

English

For any element a, inserting a into the open upper interval Ioi(a) yields the closed upper interval Ici(a); equivalently, Ioi(a) ∪ {a} = Ici(a).

Русский

Для любого a множество, получаемое добавлением a в открытое верхнее множество Ioi(a), равно закрытому верхнему интервалу Ici(a); то есть Ioi(a) ∪ {a} = Ici(a).

LaTeX

$$$ Ioi(a) \cup \{a\} = Ici(a) $$$

Lean4

@[simp]
theorem Ioi_insert [DecidableEq α] (a : α) : insert a (Ioi a) = Ici a :=
  by
  ext
  simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]

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