Theorems · Theorem · order theory

Set.image2_subset_iff

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {u : Set γ},
  Set.image2 f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u

Defined in

Mathlib.Data.Set.NAry

Cited by

30 results in Mathlib

Foundations

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