Theorems · Theorem · order theory

iSup_iUnion

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} [inst : CompleteLattice β] (s : ι → Set α) (f : α → β),
  ⨆ a ∈ ⋃ i, s i, f a = ⨆ i, ⨆ a ∈ s i, f a

Defined in

Mathlib.Data.Set.Lattice

Cited by

5 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext, Quot.sound

Assumes

CompleteLattice