Theorems · Theorem · order theory

Set.Finite.biSup_iInf_eq

∀ {α : Type u} {ι : Type v} {κ : ι → Sort w} [Nonempty ((a : ι) → κ a)] [inst : Order.Coframe α] {s : Set ι},
  s.Finite → ∀ {f : (a : ι) → κ a → α}, ⨆ a ∈ s, ⨅ b, f a b = ⨅ g, ⨆ a ∈ s, f a (g a)

Defined in

Mathlib.Data.Set.Finite.Lattice

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonemptyOrder.Coframe