finsetImage_val_uIcc — Mathlib

English

The Nat-valued image of the closed interval uIcc(a,b) equals the Nat interval uIcc(a.val,b.val).

Русский

Изображение в ℕ замкнутого интервала uIcc(a,b) через вложение равно uIcc(a.val,b.val).

LaTeX

$$$(\operatorname{Finset.uIcc}\ a\ b).\mathrm{image}\ \mathrm{val} = \operatorname{Finset.uIcc}(a.\mathrm{val}, b.\mathrm{val})$$$

Lean4

@[simp]
theorem finsetImage_val_uIcc : (uIcc a b).image val = uIcc (a : ℕ) b :=
  finsetImage_val_Icc _ _

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