Mathlib Map

Theorems · Theorem · order theory

Set.image2_empty_left

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : Set β}, Set.image2 f ∅ t = ∅
Defined in
Mathlib.Data.Set.NAry
Cited by
11 results in Mathlib
Foundations
Depth 7 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.image₂_empty_left · cited by 11Finset.image₂_empty_leftSet.empty_add · cited by 6Set.empty_addSet.empty_mul · cited by 6Set.empty_mulSet.empty_vadd · cited by 1Set.empty_vaddSet.empty_smul · cited by 1Set.empty_smulSet.empty_vsub · cited by 0Set.empty_vsubSet.empty_div · cited by 0Set.empty_divSet.empty_infs · cited by 0Set.empty_infsSet.empty_sdiv · cited by 0Set.empty_sdivSet.empty_sub · cited by 0Set.empty_subSet.empty_sups · cited by 0Set.empty_supsSet · cited by 53352SetSet.ext · cited by 2266Set.extSet.image2 · cited by 311Set.image2Set.image2_empty_leftCITED BYCITES

Cites3

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.extproof · cited by 2,266
  • Set.image2statement · cited by 311

Cited by11

Results whose statement or proof uses this declaration.