Theorems · Theorem · order theory

Set.forall_mem_image2

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β} {p : γ → Prop},
  (∀ z ∈ Set.image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)

Defined in

Mathlib.Data.Set.NAry

Cited by

20 results in Mathlib

Foundations

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