Theorems · Theorem · order theory

Finset.apply_sup_eq_sup_comp

∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  [inst_2 : SemilatticeSup γ] [inst_3 : OrderBot γ] {s : Finset β} {f : β → α} (g : α → γ),
  (∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) → g ⊥ = ⊥ → g (s.sup f) = s.sup (g ∘ f)

Defined in

Mathlib.Data.Finset.Lattice.Fold

Cited by

11 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemilatticeSupOrderBotSemilatticeSupOrderBot