Mathlib Map

Theorems · Theorem · combinatorics

Finset.pimage_subset

∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
  {s : Finset α} {t : Finset β}, Finset.pimage f s ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t
Defined in
Mathlib.Data.Finset.PImage
Cited by
1 results in Mathlib
Foundations
Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEqDecidable
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Finset.pimage_mono · cited by 0Finset.pimage_monoFinset · cited by 13712FinsetPart · cited by 325PartPFun · cited by 207PFunPart.Dom · cited by 145Part.DomFinset.pimage · cited by 11Finset.pimageFinset.pimage_subsetCITED BYCITES

Cites5

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

  • Finsetstatement and proof · cited by 13,712
  • Partstatement · cited by 325
  • PFunstatement and proof · cited by 207
  • Part.Domstatement and proof · cited by 145
  • Finset.pimagestatement · cited by 11

Cited by1

Results whose statement or proof uses this declaration.