instInfSet — Mathlib

English

There exists a canonical InfSet structure on the naturals; in particular, the Infimum sInf s is defined as the least element of s when s is nonempty and is 0 for the empty set.

Русский

Существует каноническое InfSet-структура на множестве натуральных чисел; в частности, наименьшее нижнее ограничение sInf s есть наименьший элемент множества, если оно непусто, и равно 0 для пустого множества.

LaTeX

$$$sInf(s) = \begin{cases} \min s, & s \neq \emptyset \\ 0, & s = \emptyset \end{cases}$$$

Lean4

noncomputable instance : InfSet ℕ :=
  ⟨fun s ↦ if h : ∃ n, n ∈ s then @Nat.find (fun n ↦ n ∈ s) _ h else 0⟩

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