nth_strictMonoOn — Mathlib

English

If p defines a finite set hf, then the function n ↦ nth p n is strictly monotone on the interval {0,1,...,#hf.toFinset − 1}.

Русский

Если p задаёт конечное множество hf, то функция n ↦ nth p n строго возрастает на интервале {0,..., |hf.toFinset| − 1}.

LaTeX

$$StrictMonoOn (nth p) (Set.Iio #hf.toFinset)$$

Lean4

theorem nth_strictMonoOn (hf : (setOf p).Finite) : StrictMonoOn (nth p) (Set.Iio #hf.toFinset) :=
  by
  rintro m (hm : m < _) n (hn : n < _) h
  simp only [nth_eq_orderEmbOfFin, *]
  exact OrderEmbedding.strictMono _ h

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