Theorems · Theorem · logic and foundations

Set.mem_image2_of_mem

∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β},
  a ∈ s → b ∈ t → f a b ∈ Set.image2 f s t

Defined in

Mathlib.Data.Set.Operations

Cited by

40 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms