quot.forall

Stream: Is there code for X?

[Eric Wieser]

Do we really not have this?

lemma quot.forall {α} {r : α → α → Prop} {C : quot r → Prop} :
  (∀ x : quot r, C x) ↔ ∀ x : α, C (quot.mk r x) :=
⟨λ hx x, hx _, quot.ind⟩

I was sure I saw some variant of it somewhere. Obviously we'd want it for quotient.mk, ideal.quotient.mk, etc too{

[Eric Wieser]

Oh, I guess you can prove it with quotient.surjective_quotient_mk'.forall

[Yury G. Kudryashov]

You probably mean surjective_quot_mk.

[Eric Wieser]

Right, that's the one that actually matches my theorem statement syntactically

[Eric Wieser]

Do you think we should have the forall lemma for each quotient constructor anyway, or should we just sure we have a proof of surjectivity for each of our plethora of aliases of quot.mk