Theorems · Theorem · order theory

Set.image2_assoc

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} {ε : Type u_9} {ε' : Type u_10} {s : Set α} {t : Set β}
  {u : Set γ} {f : δ → γ → ε} {g : α → β → δ} {f' : α → ε' → ε} {g' : β → γ → ε'},
  (∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)) →
    Set.image2 f (Set.image2 g s t) u = Set.image2 f' s (Set.image2 g' t u)

Defined in

Mathlib.Data.Set.NAry

Cited by

6 results in Mathlib

Foundations

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