Commit 2023-07-06 05:37 7bc03a76

View on Github →

feat: UnivLE (#5723)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/UnivLE.lean

added theorem UnivLE.ofEssSurj.{u,

added def UnivLE.witness.{u,

added theorem UnivLE_iff_essSurj.{u,

Created Mathlib/Logic/UnivLE.lean