instLocallyFiniteOrder — Mathlib

English

Let n ∈ ℕ. The set Fin(n) with its standard order is locally finite; the finite intervals Icc, Ico, Ioc, Ioo are finite and correspond to the natural-number intervals via the natural embedding.

Русский

Пусть n ∈ ℕ. Множество Fin(n) с обычным порядком локально конечно; конечные интервалы Icc, Ico, Ioc, Ioo конечны и соответствуют соответствующим интервалам в ℕ через естественную вложенность.

LaTeX

$$$\text{Fin}(n)$ is locally finite; \ Icc, Ico, Ioc, Ioo are finite and realized by the standard embedding from ℕ to Fin(n).$$

Lean4

instance instLocallyFiniteOrder (n : ℕ) : LocallyFiniteOrder (Fin n)
    where
  finsetIcc a b := attachFin (Icc a b) fun x hx ↦ (mem_Icc.mp hx).2.trans_lt b.2
  finsetIco a b := attachFin (Ico a b) fun x hx ↦ (mem_Ico.mp hx).2.trans b.2
  finsetIoc a b := attachFin (Ioc a b) fun x hx ↦ (mem_Ioc.mp hx).2.trans_lt b.2
  finsetIoo a b := attachFin (Ioo a b) fun x hx ↦ (mem_Ioo.mp hx).2.trans b.2
  finset_mem_Icc a b := by simp
  finset_mem_Ico a b := by simp
  finset_mem_Ioc a b := by simp
  finset_mem_Ioo a b := by simp

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