le_of_nth_le_nth_of_lt_card — Mathlib

English

If the set {n : ℕ | p n} is finite, and nth p m ≤ nth p n with m < card of that set, then m ≤ n.

Русский

Если множество {n : ℕ | p n} конечно, и nth p m ≤ nth p n при m < кардинал этого множества, то m ≤ n.

LaTeX

$$$hf : (\\{n : \\mathbb{N} | p(n)\\}).Finite \\Rightarrow (h : nth\\ p\\ m \\le nth\\ p\\ n) \\to (hm : m < |hf|) \\Rightarrow m \\le n.$$$

Lean4

theorem le_of_nth_le_nth_of_lt_card (hf : (setOf p).Finite) {m n : ℕ} (h : nth p m ≤ nth p n) (hm : m < #hf.toFinset) :
    m ≤ n :=
  not_lt.1 fun hlt => h.not_gt <| nth_lt_nth_of_lt_card hf hlt hm

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