def Fintype.sup {ι : Type u_1} [Fintype ι] {α : Type u_2} [SemilatticeSup α] [OrderBot α] (f : ι → α) : α

Equations

• Fintype.sup f = Finset.univ.sup f

@[simp]

theorem Fintype.elem_le_sup {ι : Type u_2} [Fintype ι] {α : Type u_1} [SemilatticeSup α] [OrderBot α] (f : ι → α) (i : ι) : f i ≤ sup f

theorem Fintype.le_sup {ι : Type u_2} [Fintype ι] {α : Type u_1} [SemilatticeSup α] [OrderBot α] {a : α} {f : ι → α} (i : ι) (le : a ≤ f i) : a ≤ sup f

@[simp]

theorem Fintype.sup_le_iff {ι : Type u_2} [Fintype ι] {α : Type u_1} [SemilatticeSup α] [OrderBot α] {f : ι → α} {a : α} : sup f ≤ a ↔ ∀ (i : ι), f i ≤ a

@[simp]

theorem Fintype.finsup_eq_0_of_empty {ι : Type u_1} [Fintype ι] {α : Type u_2} [SemilatticeSup α] [OrderBot α] [IsEmpty ι] (f : ι → α) : sup f = ⊥

def Fintype.decideEqPi {ι : Type u_2} [Fintype ι] {β : ι → Type u_1} (a b : (i : ι) → β i) : ((i : ι) → Decidable (a i = b i)) → Decidable (a = b)

Equations

• Fintype.decideEqPi a b x✝ = decidable_of_iff (∀ (i : ι), a i = b i) ⋯