max_union

Mathlib.Data.Finset.Max

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

English

The maximum of the union of two Finsets equals the join of their maxima.

Русский

Максимум объединения двух конечных множеств равен объединению их максимумов.

LaTeX

$$$\max(s \cup t) = \max(s) \sqcup \max(t)$$$

Lean4

theorem max_union {s t : Finset α} : (s ∪ t).max = s.max ⊔ t.max :=
  sup_union

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

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

Разделы

Аффилиация

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