finite_range_findGreatest — Mathlib

English

For any P: α → Nat → Prop with decidable predicates, the range of x ↦ Nat.findGreatest(P x) is finite.

Русский

Для любого P: α → Nat → Prop с разрешимыми предикатами множество Nat.findGreatest(P x) по x конечно.

LaTeX

$$$ \text{Finite} \bigl( \{ Nat.findGreatest (P x) b : x \in α \} \bigr) $$$

Lean4

theorem finite_range_findGreatest {P : α → ℕ → Prop} [∀ x, DecidablePred (P x)] {b : ℕ} :
    (range fun x => Nat.findGreatest (P x) b).Finite :=
  (finite_le_nat b).subset <| range_subset_iff.2 fun _ => Nat.findGreatest_le _

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