Theorem: Fintype.sup_le_iff (Logic/Vorspiel/Vorspiel.lean)

State before:
ι : Type u_2
inst✝² : Fintype ι
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : ι → α
a : α
⊢ sup f ≤ a ↔ ∀ (i : ι), f i ≤ a
Tactic:
simp[sup]
State after:
no goals