Theorems · Theorem · order theory

Set.image2_nonempty_iff

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
  (Set.image2 f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Defined in: Mathlib.Data.Set.NAry
Cited by: 14 results in Mathlib
Foundations: Depth 7 from the axioms · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.Nonemptystatement and proof · cited by 2,627
Set.image2statement and proof · cited by 311
Set.Nonempty.image2proof · cited by 14

Cited by14

Results whose statement or proof uses this declaration.

Finset.image₂_nonempty_iffproof · cited by 14
Set.Nonempty.of_image2_leftproof · cited by 12
Set.Nonempty.of_image2_rightproof · cited by 12
Set.image2_eq_empty_iffproof · cited by 10
Set.div_nonemptyproof · cited by 0
Set.vadd_nonemptyproof · cited by 0
Set.mul_nonemptyproof · cited by 0
Set.sub_nonemptyproof · cited by 0
Set.sups_nonemptyproof · cited by 0
Set.add_nonemptyproof · cited by 0
Set.sdiv_nonemptyproof · cited by 0
Set.smul_nonemptyproof · cited by 0