sup_le — Mathlib

English

For a multiset s and an element a, sup(s) ≤ a if and only if every b in s satisfies b ≤ a.

Русский

Для мультсета s и элемента a выполняется: sup(s) ≤ a тогда и только тогда, когда каждый элемент s ≤ a.

LaTeX

$$$\\operatorname{sup}(s) \\le a \\;\\iff\\; \\forall b \\in s,\\ b \\le a$$$

Lean4

@[simp]
theorem sup_le {s : Multiset α} {a : α} : s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a :=
  Multiset.induction_on s (by simp) (by simp +contextual [or_imp, forall_and])

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