Mathlib Map

Theorems · Theorem · logic and foundations

PFun.preimage_comp

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (s : Set γ),
  (f.comp g).preimage s = g.preimage (f.preimage s)
Defined in
Mathlib.Data.PFun
Cited by
0 results in Mathlib
Foundations
Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set · cited by 53352SetPFun · cited by 207PFunPFun.preimage · cited by 18PFun.preimagePFun.comp · cited by 10PFun.compPFun.preimage_compCITED BYCITES

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
  • PFunstatement and proof · cited by 207
  • PFun.preimagestatement · cited by 18
  • PFun.compstatement · cited by 10

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.