exists_notMem_of_gt — Mathlib

English

If s is PartiallyWellOrderedOn r and f is strictly decreasing with respect to r along indices, then there exists k such that for all m > k, f(m) ∉ s.

Русский

Если s частично хорошо упорядочено по r и f убывает по порядку, то найдется k, после которого все f(m) не принадлежат s.

LaTeX

$$∃ k : ℕ, ∀ m, k < m → f m ∉ s$$

Lean4

theorem exists_notMem_of_gt {s : Set α} (hs : s.PartiallyWellOrderedOn r) {f : ℕ → α}
    (hf : ∀ m n : ℕ, m < n → ¬r (f m) (f n)) : ∃ k : ℕ, ∀ m, k < m → f m ∉ s :=
  by
  have := hs.bddAbove_preimage hf
  contrapose! this
  simpa [not_bddAbove_iff, and_comm]

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