English
The value produced by the bounded greatest function is independent of the precise lower bound, hence two instances produced with possibly different bounds but satisfying the same predicate yield the same greatest value when viewed as integers.
Русский
Значение, получаемое функцией наибольшего при ограниченной сфере, не зависит от конкретной нижней границы; два случая с разными пределами, удовлетворяющими одному и тому же предикату, дают одинаковое наибольшее значение.
LaTeX
$$$\forall P : \mathbb{Z} \to \mathrm{Prop} \ [\mathrm{DecidablePred} \ P] \forall b \forall Hb \forall Hinh,\ (P \; \text{ub}) \land \forall z\; (P(z) \rightarrow z \le \text{ub}) \Rightarrow \, \text{ub in integers} \; (\text{greatestOfBdd}\ b\ Hb\ Hinh) = \text{greatestOfBdd}\ b'\ Hb'\ Hinh$$
Lean4
/-- `Int.greatestOfBdd` is the greatest integer satisfying a predicate which is false for all
`z : ℤ` with `b < z` for some fixed `b : ℤ`. -/
theorem isGreatest_coe_greatestOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → z ≤ b)
(Hinh : ∃ z : ℤ, P z) : IsGreatest {z | P z} (greatestOfBdd b Hb Hinh : ℤ) :=
(greatestOfBdd b Hb Hinh).2
