Theorems · Theorem · order theory

Set.image2_range

∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} (f : α' → β' → γ) (g : α → α')
  (h : β → β'), Set.image2 f (Set.range g) (Set.range h) = Set.range fun x => f (g x.1) (h x.2)

Defined in

Mathlib.Data.Set.NAry

Cited by

2 results in Mathlib

Foundations

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