attachFin_Icc — Mathlib

English

For a,b ∈ Fin(n), the Icc interval in Fin(n) agrees with the attached version of Icc(a.val,b.val); i.e., the two Finsets are equal.

Русский

Для a,b ∈ Fin(n) интервалы Icc в Fin(n) совпадают с прикреплённой версией Icc(a.val, b.val); то есть два множества Fin совпадают.

LaTeX

$$$\operatorname{attachFin}(\mathrm{Icc}(a,b),\dots) = \mathrm{Icc}(a,b).$$$

Lean4

@[simp]
theorem attachFin_Icc : attachFin (Icc a b) (fun _x hx ↦ (mem_Icc.mp hx).2.trans_lt b.2) = Icc a b :=
  rfl

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