Code

feat(Topology): the ULift functor#20345

Code

Open

joelriou wants to merge 6 commits intomasterleanprover-community/mathlib4:masterfrom topcat-uliftfunctorleanprover-community/mathlib4:topcat-uliftfunctorCopy head branch name to clipboard

+72-1

Commits

Commits on Dec 30, 2024

• feat(Topology): the ULift functor

  joelriou

  committed
  df42a14

  Copy full SHA for df42a14

• better name

  joelriou

  committed
  ea66e85

  Copy full SHA for ea66e85

Commits on Jan 1, 2025

• Merge remote-tracking branch 'origin' into topcat-uliftfunctor

  joelriou

  committed
  d31c413

  Copy full SHA for d31c413

• using ULift.map, added FullyFaithful

  joelriou

  committed
  fcd046e

  Copy full SHA for fcd046e

• removed unnecessary lines

  joelriou

  committed
  4ae3368

  Copy full SHA for 4ae3368

Commits on Jan 25, 2025

• Update Mathlib/Topology/Category/TopCat/ULift.lean

  joelriou

  authored
  5eb5f12

  Copy full SHA for 5eb5f12