find_min' — Mathlib

English

The found index is minimal among all indices with p.

Русский

Найденный индекс минимален среди всех индексов, удовлетворяющих p.

LaTeX

$$$$ \text{For all } i, j, \ p j \Rightarrow i \le j \text{ whenever } i \in \mathrm{Fin.find}\ p $$$$

Lean4

theorem find_min' {p : Fin n → Prop} [DecidablePred p] {i : Fin n} (h : i ∈ Fin.find p) {j : Fin n} (hj : p j) :
    i ≤ j :=
  Fin.not_lt.1 fun hij ↦ find_min h hij hj

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