English
Let P be a predicate on the integers with a decidability assumption. If b and b' are integers such that every z with P(z) satisfies z ≥ b and also z ≥ b', and additionally P holds for some z, then the least element among z with P(z) bounded below by b coincides with the least element bounded below by b'. In other words, the least element is independent of the particular lower bound used, provided it is a valid lower bound.
Русский
Пусть P — предикат на множествах целых чисел, и существует доказательство допуска. Пусть b, b' ∈ ℤ такие, что для всех z ∈ ℤ, если P(z), то b ≤ z и также b' ≤ z, и существует z с P(z). Тогда наименьший элемент среди z, удовлетворяющих P, при условии z ≥ b, равен наименьшему элементу при условии z ≥ b'. Формально: наименьший элемент не зависит от выбора нижней границы.
LaTeX
$$$\\forall P : \\mathbb{Z} \\to \\mathrm{Prop} \\, [\\mathrm{DecidablePred} \\ P] \; \\forall b \; \\forall b' \;\\big( (\\forall z : \\mathbb{Z},\\ P(z) \\rightarrow b \\le z) \\land (\\forall z : \\mathbb{Z},\\ P(z) \\rightarrow b' \\le z) \\land (\\exists z : \\mathbb{Z}, P(z)) \\rightarrow \\, (\\mathrm{leastOfBdd} \\, b \\, Hb \\, Hinh = \\mathrm{leastOfBdd} \\, b' \\, Hb' \\, Hinh) \\big)$$$
Lean4
theorem coe_leastOfBdd_eq {P : ℤ → Prop} [DecidablePred P] {b b' : ℤ} (Hb : ∀ z : ℤ, P z → b ≤ z)
(Hb' : ∀ z : ℤ, P z → b' ≤ z) (Hinh : ∃ z : ℤ, P z) : (leastOfBdd b Hb Hinh : ℤ) = leastOfBdd b' Hb' Hinh := by
grind
