Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-26 12:04 f92e8124

View on Github →

feat(data/setoid): create file about setoids (#1453)

  • setoid complete lattice
  • order iso and Galois insertion
  • added documentation
  • editing docstrings
  • not opening lattice twice
  • partitions
  • typo
  • minor edits
  • editing docstrings
  • applying review comments
  • editing implementation notes
  • partly applied review comments
  • moved length_scanl
  • whoops, and removed length_scanl from setoid
  • editing implementation notes
  • generalising of_quotient a bit more
  • style tweaks + reviewer changes
  • removing Bell numbers for now
  • revert docstring
  • applying review comments
  • generalising to_quotient
  • partly applying review comments
  • applying review comments
  • readding list length lemmas

Estimated changes

added theorem list.last_eq_nth_le
added theorem list.length_scanl
added theorem set.disjoint_left
added theorem set.disjoint_right
added theorem set.sUnion_eq_univ_iff
added theorem quotient.eq_rel
added theorem setoid.Inf_def
added theorem setoid.Inf_le
added theorem setoid.Sup_def
added theorem setoid.Sup_eq_eqv_gen
added def setoid.classes
added theorem setoid.classes_inj
added def setoid.comap
added theorem setoid.eq_iff_rel_eq
added theorem setoid.eqv_class_mem
added theorem setoid.eqv_gen_eq
added theorem setoid.eqv_gen_idem
added theorem setoid.eqv_gen_le
added theorem setoid.eqv_gen_mono
added theorem setoid.ext'
added theorem setoid.ext_iff
added def setoid.gi
added theorem setoid.inf_def
added theorem setoid.inf_iff_and
added def setoid.ker
added theorem setoid.ker_mk_eq
added theorem setoid.le_Inf
added theorem setoid.le_def
added theorem setoid.lift_unique
added def setoid.map
added theorem setoid.mem_classes
added theorem setoid.refl'
added def setoid.rel
added theorem setoid.sup_def
added theorem setoid.sup_eq_eqv_gen
added theorem setoid.symm'
added theorem setoid.trans'