Zulip Chat Archive

Stream: general

Topic: nonempty quotient


view this post on Zulip Patrick Massot (Sep 30 2018 at 20:05):

Do we already have something like:

lemma nonempty_quotient_iff {α : Type*} (s : setoid α) : nonempty (quotient s)  nonempty α :=
begin
  split ; rintro c,
  { cases quotient.exists_rep c with a h,
    exact a },
  { exact c }
end

view this post on Zulip Simon Hudon (Sep 30 2018 at 20:56):

That would be in data/quot and I don't see it there.


Last updated: May 10 2021 at 18:22 UTC