instLocallyFiniteOrder — Mathlib

English

The integers with the usual order form a locally finite order: for any a ≤ b, the interval [a,b] is finite and has size b−a+1.

Русский

Целые числа с обычным порядком образуют локально конечный порядок: для любых a ≤ b промежуток [a,b] конечен и имеет размер b−a+1.

LaTeX

$$$$\\forall a,b \\in \\mathbb{Z},\\ a \\le b \\Rightarrow \\lvert\\{x \\in \\mathbb{Z} : a \\le x \\le b\\}\\rvert = b - a + 1.$$$$

Lean4

instance instLocallyFiniteOrder : LocallyFiniteOrder ℤ
    where
  finsetIcc a b := (Finset.range (b + 1 - a).toNat).map <| Nat.castEmbedding.trans <| addLeftEmbedding a
  finsetIco a b := (Finset.range (b - a).toNat).map <| Nat.castEmbedding.trans <| addLeftEmbedding a
  finsetIoc a b := (Finset.range (b - a).toNat).map <| Nat.castEmbedding.trans <| addLeftEmbedding (a + 1)
  finsetIoo a b := (Finset.range (b - a - 1).toNat).map <| Nat.castEmbedding.trans <| addLeftEmbedding (a + 1)
  finset_mem_Icc a b
    x :=
    by
    simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply, addLeftEmbedding_apply]
    constructor
    · omega
    · intro
      use (x - a).toNat
      omega
  finset_mem_Ico a b
    x :=
    by
    simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply, addLeftEmbedding_apply]
    constructor
    · omega
    · intro
      use (x - a).toNat
      omega
  finset_mem_Ioc a b
    x :=
    by
    simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply, addLeftEmbedding_apply]
    constructor
    · omega
    · intro
      use (x - (a + 1)).toNat
      omega
  finset_mem_Ioo a b
    x :=
    by
    simp_rw [mem_map, mem_range, Function.Embedding.trans_apply, Nat.castEmbedding_apply, addLeftEmbedding_apply]
    constructor
    · omega
    · intro
      use (x - (a + 1)).toNat
      omega

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