Mathlib Map

Theorems · Theorem · order theory

Set.subset_fst_image_prod_snd_image

∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)}, s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)
Defined in
Mathlib.Data.Set.Prod
Cited by
3 results in Mathlib
Foundations
Depth 10 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AddAction.properVAdd_iff_isCompact_setOfPred_inter_nonempty · cited by 2AddAction.properVAdd_iff_…MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty · cited by 1MulAction.properSMul_iff_…Monotone.upperBounds_image_of_directedOn_prod · cited by 1Monotone.upperBounds_imag…Set · cited by 53352SetSet.image · cited by 5609Set.imageSProd.sprod · cited by 1750SProd.sprodSet.subset_fst_image_prod_snd…CITED 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.imagestatement and proof · cited by 5,609
  • SProd.sprodstatement and proof · cited by 1,750

Cited by3

Results whose statement or proof uses this declaration.