Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-25 02:14 84582d28

View on Github →

feat(data/quot,data/set/basic): add lemmas about lift (#17699)

  • Add quot.surjective_lift, quotient.surjective_lift_on'.
  • Mark quot.lift_mk as simp.
  • Add set.range_quot_lift, set.range_quotient_lift, set.range_quotient_mk', and set.range_quotient_lift_on'.
  • The mathlib4 version: leanprover-community/mathlib4#701.
  • Prove matrix.to_linear_map₂_apply by rfl.

Estimated changes

added theorem quot.surjective_lift
modified theorem quotient.out_injective
modified theorem surjective_quot_mk
added theorem set.range_quot_lift
added theorem set.range_quotient_mk'