sup_le_iff — Mathlib

English

For any a, s.sup f ≤ a is equivalent to f(b) ≤ a for all b ∈ s.

Русский

Для любого a верхняя грань над s равна или меньше a тогда и только тогда все f(b) ≤ a для всех b ∈ s.

LaTeX

$$$ s.sup f \\le a \\iff \\forall b \\in s, f b \\le a $$$

Lean4

@[simp]
protected theorem sup_le_iff {a : α} : s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a :=
  by
  apply Iff.trans Multiset.sup_le
  simp only [Multiset.mem_map, and_imp, exists_imp]
  exact ⟨fun k b hb => k _ _ hb rfl, fun k a' b hb h => h ▸ k _ hb⟩

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