Mathlib Map

Theorems · Theorem · combinatorics

Finset.pimage.congr_simp

∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f f_1 : α →. β),
  f = f_1 →
    ∀ {inst_1 : (x : α) → Decidable (f x).Dom} [inst_2 : (x : α) → Decidable (f_1 x).Dom] (s s_1 : Finset α),
      s = s_1 → Finset.pimage f s = Finset.pimage f_1 s_1
Defined in
Mathlib.Data.Finset.PImage
Cited by
0 results in Mathlib
Foundations
Depth 75 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 · cited by 13712FinsetPFun · cited by 207PFunPart.Dom · cited by 145Part.DomFinset.pimage · cited by 11Finset.pimagepimage.congr_simpCITED BYCITES

Cites4

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
  • PFunstatement and proof · cited by 207
  • Part.Domstatement and proof · cited by 145
  • Finset.pimagestatement and proof · cited by 11

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.