Theorems · Theorem · order theory

Set.Finite.biInf_iSup_eq

∀ {α : Type u} {ι : Type v} {κ : ι → Sort w} [Nonempty ((a : ι) → κ a)] [inst : Order.Frame α] {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

1 results in Mathlib

Foundations

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

Assumes

NonemptyOrder.Frame