iff.intro quotient.exact' quotient.sound'

Stream: Is there code for X?

[Eric Wieser]

Does this have a name? If not, what would be a good name for it?

[Johan Commelin]

I have no idea what the types of quotient.exact' and quotient.sound' are... so I don't know what this question is :wink:

[Eric Wieser]

I will update with the statement shortly...

[Eric Wieser]

lemma quotient.name_me {α : Type*} (x y : α) [s : setoid α] :
  quotient.mk x = quotient.mk y ↔ x ≈ y :=
⟨quotient.exact, quotient.sound⟩

lemma quotient.name_me' {α : Type*} (x y : α) (s : setoid α) :
  (quotient.mk' x : quotient s) = quotient.mk' y ↔ setoid.r x y :=
⟨quotient.exact', quotient.sound'⟩

(xref: docs#quotient.exact, docs#quotient.exact', docs#quotient.sound, docs#quotient.sound')

[Eric Wieser]

Ah, it's docs#quotient.eq'

[Kevin Buzzard]

Your question reminds me that somewhere deep down in my job list is "write basic document on quotients explaining all the language used in mathlib"

[Kevin Buzzard]

For mathematicians it's particularly confusing, because we traditionally use lift to mean something else.

[Eric Wieser]

It probably doesn't help that the definitions and therefore documentation is split between core and mathlib