max_eq_top

Mathlib.Data.Finset.Max

URI: https://scilib.ai/kg/mathlib#Finset.max_eq_top

English

In an OrderTop, max s equals top exactly when top ∈ s.

Русский

В порядке с верхней границей max s равен top тогда и только тогда, когда top ∈ s.

LaTeX

$$$s_{\max} = \top \iff \top \in s$$$

Lean4

@[simp]
protected theorem max_eq_top [OrderTop α] {s : Finset α} : s.max = ⊤ ↔ ⊤ ∈ s :=
  Finset.sup_eq_top_iff.trans <| by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru