isLeast_bot_iff — Mathlib

English

In a preorder with a bottom element, s has ⊥ as a least element if and only if ⊥ ∈ s.

Русский

В предпорядке с нулевой границей множество s имеет ⊥ как наименьший элемент тогда и только тогда, когда ⊥ ∈ s.

LaTeX

$$$\\IsLeast s \\bot \\iff \\bot \\in s$$$

Lean4

@[simp]
theorem isLeast_bot_iff [OrderBot α] : IsLeast s ⊥ ↔ ⊥ ∈ s :=
  and_iff_left <| bot_mem_lowerBounds _

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