Iio_eq_finset_subtype — Mathlib

English

Let n ∈ ℕ and b ∈ Fin n. Then the Fin-set Iio b inside Fin n is equal to the finset obtained from Iio b.val in ℕ via fin n.

Русский

Пусть n ∈ ℕ и b ∈ Fin n. Тогда Fin-овское множество Iio b внутри Fin n равно финсет, полученному из Iio b.val в ℕ через fin n.

LaTeX

$$$Iio\,b = (Iio\,(b.\mathrm{val})).\mathrm{fin}\,n$$$

Lean4

@[deprecated attachFin_Iio (since := "2025-04-06")]
theorem Iio_eq_finset_subtype : Iio b = (Iio (b : ℕ)).fin n := by ext; simp

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