nth_lt_nth_of_lt_card

Mathlib.Data.Nat.Nth

URI: https://scilib.ai/kg/mathlib#Nat.nth_lt_nth_of_lt_card

← MathLib Explorer

English

If hf is finite, and m < n < |hf.toFinset|, then nth p m < nth p n.

Русский

Если hf конечное и m < n < |hf.toFinset|, то nth p m < nth p n.

LaTeX

$$For hf finite, if m < n < #hf.toFinset then nth p m < nth p n.$$

Lean4

theorem nth_lt_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : m < n) (hn : n < #hf.toFinset) :
    nth p m < nth p n :=
  nth_strictMonoOn hf (h.trans hn) hn h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru