Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-26 13:38 0fc4e6a8

View on Github →

refactor(data/set/function): move function.restrict to set, redefine (#2243)

  • refactor(data/set/function): move function.restrict to set, redefine We had subtype.restrict and function.restrict both defined in the same way using subtype.val. This PR moves function.restrict to set.restrict and makes it use coe instead of subtype.val.
  • Fix compile
  • Update src/data/set/function.lean

Estimated changes

deleted theorem set.subtype.val_range
modified theorem subtype.val_range
added def set.cod_restrict
modified theorem set.range_restrict
added def set.restrict
added theorem set.restrict_apply
added theorem set.restrict_eq
modified theorem subtype.val_eq_coe
deleted def function.restrict
deleted theorem function.restrict_eq
deleted theorem antilipschitz_with.id
modified theorem subtype.dist_eq
modified theorem subtype.edist_eq