instDecidableIsLeast — Mathlib

English

The set of upper bounds of s consists of all elements x such that a ≤ x for every a ∈ s.

Русский

Множество верхних границ s состоит из всех элементов x такие, что a ≤ x для каждого a ∈ s.

LaTeX

$$$\\operatorname{upperBounds}(s) = \\{ x \\in \\alpha \\mid \\forall a\\in s,\ a \\le x \\}$$$

Lean4

instance instDecidableIsLeast (p : ℕ → Prop) (n : ℕ) [DecidablePred p] : Decidable (IsLeast {n : ℕ | p n} n) :=
  decidable_of_iff (p n ∧ ∀ k < n, ¬p k) <| .and .rfl <| by simp [mem_lowerBounds, @imp_not_comm _ (p _)]

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