isLeast_coe_leastOfBdd — Mathlib

English

The element produced by leastOfBdd is the least element of the set {z | P(z)} when viewed as a subtype element.

Русский

Элемент, полученный из leastOfBdd, является наименьшим элементом множества {z | P(z)} в виде подтипа.

LaTeX

$$IsLeast {z | P(z)} (leastOfBdd Hb Hinh).val$$

Lean4

/-- `Int.leastOfBdd` is the least integer satisfying a predicate which is false for all `z : ℤ` with
`z < b` for some fixed `b : ℤ`. -/
theorem isLeast_coe_leastOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ, P z → b ≤ z)
    (Hinh : ∃ z : ℤ, P z) : IsLeast {z | P z} (leastOfBdd b Hb Hinh : ℤ) :=
  (leastOfBdd b Hb Hinh).2

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