min_eq_bot — Mathlib

English

Let α be an ordered set with bottom ⊥. For a finite nonempty set S, min S = ⊥ if and only if ⊥ ∈ S.

Русский

Пусть α имеет минимум ⊥. Для конечного непустого множества S верно: min S = ⊥ тогда и только тогда, когда ⊥ ∈ S.

LaTeX

$$$$\min S = \perp \iff \perp \in S.$$$$

Lean4

@[simp]
protected theorem min_eq_bot [OrderBot α] {s : Finset α} : s.min = ⊥ ↔ ⊥ ∈ s :=
  Finset.max_eq_top (α := αᵒᵈ)

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