Theorems · Definition · category theory
Function.Fiber.mk
{Y : Type u_2} → {Z : Type u_3} → (f : Y → Z) → Y → Function.Fiber fGiven y : Y, Fiber.mk f y is the fiber of f that y belongs to, as an element of Fiber f.
- Defined in
- Mathlib.Logic.Function.FiberPartition
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.preimageproof · cited by 4,946
- Function.Fiberstatement · cited by 18
Cited by6
Results whose statement or proof uses this declaration.
- Function.Fiber.mkSelfstatement · cited by 1
- Function.Fiber.mk_imagestatement and proof · cited by 1
- CompHausLike.LocallyConstant.componentHomstatement · cited by 1
- CompHausLike.LocallyConstant.incl_comapstatement · cited by 0
- TopologicalSpace.Fiber.sigmaInclInclstatement · cited by 0
- Function.Fiber.image_eq_image_mkstatement and proof · cited by 0