coe_bot — Mathlib

English

Let s ⊆ ℕ be nonempty. The bottom element of s, as a natural number, equals the least element of s.

Русский

Пусть s ⊆ ℕ непусто. Нижний элемент s, как число, равен наименьшему элементу s.

LaTeX

$$$$ \forall s\subseteq \mathbb{N},\ s \neq \varnothing \Rightarrow \operatorname{bot}(s)=\min s. $$$$

Lean4

theorem coe_bot {s : Set ℕ} [DecidablePred (· ∈ s)] [h : Nonempty s] :
    ((⊥ : s) : ℕ) = Nat.find (nonempty_subtype.1 h) :=
  rfl

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