Theorems · Theorem · order theory

iInf_image2

∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_8} {δ : Type u_9} (f : β → γ → δ) (s : Set β)
  (t : Set γ) (g : δ → α), ⨅ d ∈ Set.image2 f s t, g d = ⨅ b ∈ s, ⨅ c ∈ t, g (f b c)

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompleteLattice