finsetImage_val_Ioc — Mathlib

English

The Nat-valued image of the half-open interval Ioc(a,b) from Fin n equals the Nat half-open interval Ioc(a.val,b.val).

Русский

Изображение в натуральные числа половинопределённого интервала Ioc(a,b) в Fin n равно натуральному Ioc(a.val,b.val).

LaTeX

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

Lean4

@[simp]
theorem finsetImage_val_Ioc : (Ioc a b).image val = Ioc (a : ℕ) b :=
  image_val_attachFin _

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