Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-28 11:42 a6a8a11e

View on Github →

refactor(data/equiv/encodable): bring directed.sequence* from integration, use quotient.rep instead of quot.rep (#1825)

  • refactor(data/equiv/encodable): bring directed.sequence* from integration, use quotient.rep instead of quot.rep sequence_of_directed in measure_theory/integration did not belong there. Also add some docstrings.
  • doc/style fixes by @sgouezel Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • Remove an unused argument, add a docstring
  • Completely remove the reflexive r assumption

Estimated changes

added theorem directed.le_sequence
added theorem directed.rel_sequence
added theorem directed.sequence_mono
deleted def quot.rep
deleted theorem quot.rep_spec
added def quotient.rep
added theorem quotient.rep_spec
deleted theorem le_sequence_of_directed