sup_cons — Mathlib

English

Supremum of a cons equals the join of the element and the supremum of the tail: sup(a :: s) = a ⊔ sup(s).

Русский

Супремум конструирования cons равен объединению элемента и супремума хвоста: sup(a :: s) = a ⊔ sup(s).

LaTeX

$$$\\operatorname{sup}(a ::_m s) = a \\;\\sqcup\\; \\operatorname{sup}(s)$$$

Lean4

@[simp]
theorem sup_cons (a : α) (s : Multiset α) : (a ::ₘ s).sup = a ⊔ s.sup :=
  fold_cons_left _ _ _ _

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