Theorems · Theorem · order theory

sInf_image2

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ},
  sInf (Set.image2 f s t) = ⨅ a ∈ s, ⨅ b ∈ t, f a b

Defined in

Mathlib.Order.CompleteLattice.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompleteLattice