sup'_le_iff — Mathlib

English

For a finite nonempty s, s.sup' H f ≤ a if and only if f(b) ≤ a for all b ∈ s.

Русский

Для непустого конечного s выполнено: s.sup' H f ≤ a тогда и только тогда, когда f(b) ≤ a для всех b ∈ s.

LaTeX

$$$s.sup' H f \le a \iff \forall b \in s,\ f(b) \le a$$$

Lean4

@[simp]
theorem sup'_le_iff {a : α} : s.sup' H f ≤ a ↔ ∀ b ∈ s, f b ≤ a := by
  simp_rw [← @WithBot.coe_le_coe α, coe_sup', Finset.sup_le_iff]; rfl

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