isLeast_natFind — Mathlib

English

If s is a nonempty subset of ℕ, then Nat.find hs is the least element of s.

Русский

Если s непустое подмножество ℕ, то Nat.find hs является наименьшим элементом в s.

LaTeX

$$$\operatorname{IsLeast}\, s\, (\mathrm{Nat.find}\, hs)$$$

Lean4

/-- `Nat.find` is the minimum element of a nonempty set of natural numbers. -/
theorem isLeast_natFind {s : Set ℕ} [DecidablePred (· ∈ s)] (hs : s.Nonempty) : IsLeast s (Nat.find hs) :=
  Nat.isLeast_find hs

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