max_eq_bot — Mathlib

English

The maximum of a Finset equals the bottom element if and only if the Finset is empty.

Русский

Максимум конечного множества равен нижней границе тогда и только тогда, когда множество пусто.

LaTeX

$$$s_{\max} = \bot \iff s = \emptyset$$$

Lean4

theorem max_eq_bot {s : Finset α} : s.max = ⊥ ↔ s = ∅ :=
  ⟨fun h ↦
    s.eq_empty_or_nonempty.elim id fun H ↦ by
      obtain ⟨a, ha⟩ := max_of_nonempty H
      rw [h] at ha; cases ha; ,
    -- the `;` is needed since the `cases` syntax allows `cases a, b`
    fun h ↦ h.symm ▸ max_empty⟩

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