fst_natCast — Mathlib

English

Let α be a type with a preorder and a natural cast. Then for every n ∈ ℕ, the left endpoint of the interval corresponding to n is exactly n.

Русский

Пусть α обладает отношением порядка и естественным отображением целых чисел в α. Тогда для каждого n ∈ ℕ левая граница интервала, полученного из n, равна n.

LaTeX

$$$(n : \mathrm{NonemptyInterval}(\alpha)).\mathrm{fst} = n$$$

Lean4

theorem fst_natCast (n : ℕ) : (n : NonemptyInterval α).fst = n :=
  rfl

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