Topic: computers are smart??
Reid Barton (Jun 04 2018 at 15:08):
So I was going along constructing coequalizers in Top, like you do. A coequalizer is a kind of quotient, so I needed to prove that if is the quotient of by a relation, then the quotient map is continuous, so that it's a morphism in Top.
I was all set to add the lemma for that to my
continuity tactic, when I noticed the tactic had already succeeded before I did so! What happened?
Reid Barton (Jun 04 2018 at 15:09):
It turns out that continuity of the quotient map is definitionally equivalent to continuity of the identity map on , because a set is defined to be open in if and only if its preimage is open in . So the tactic found that it could just apply
Johan Commelin (Jun 04 2018 at 17:08):
Johan Commelin (Jun 05 2018 at 07:42):
In fact, Reid, how did you define the topology on ? Because there is a bunch of stuff on coinduced topologies in mathlib, and that would also give you continuity of the quotient map by definition.
Reid Barton (Jun 05 2018 at 11:52):
I did use the coinduced topology (see PR at https://github.com/leanprover/mathlib/pull/155/commits/b60f3687e8692f118c385f958d48d31388593298#diff-1c17754b46d709d0b8e22318f94035cdR903)
Johan Commelin (Jun 05 2018 at 11:53):
I see. So your
continuity tactic is not in that PR?
Last updated: May 12 2021 at 08:14 UTC