Zulip Chat Archive

Stream: new members

Topic: universal properties for topology


Aymon Wuolanne (Feb 11 2019 at 00:36):

Does mathlib already have lemmas for some universal properties? One in particular I'm interested in is for subspaces/subtypes. This is just the statement that if A is a subspace of X, and T any other space, then f : T -> A is continuous iff i o f is continuous where i is the inclusion of A into X, in this case just subtype.val.

Kenny Lau (Feb 11 2019 at 00:37):

I think it's already there

Kenny Lau (Feb 11 2019 at 00:37):

something about induced / coinduced topology

Reid Barton (Feb 11 2019 at 00:38):

It's also embedding.continuous_iff plus embedding_subtype_val

Mario Carneiro (Feb 11 2019 at 00:38):

I don't see that exact theorem, but it's an easy corollary of tendsto_subtype_rng

Mario Carneiro (Feb 11 2019 at 00:39):

or embedding_subtype_val

Kenny Lau (Feb 11 2019 at 00:42):

continuous_induced_rng?

Mario Carneiro (Feb 11 2019 at 00:44):

yes, but it needs restatement

Mario Carneiro (Feb 11 2019 at 00:44):

also couldn't that theorem be an iff?

Aymon Wuolanne (Feb 11 2019 at 00:44):

Ah yep, I think continuous_induced_rng works well enough

Aymon Wuolanne (Feb 11 2019 at 00:45):

I only needed the forward direction, but it probably could be restated as an iff yeah

Kenny Lau (Feb 11 2019 at 00:45):

you simp-minded people /s

Mario Carneiro (Feb 11 2019 at 00:47):

Haven't I mentioned before that over-reliance on defeq is an anti-pattern that leads to non-modularity and code brittleness?

Mario Carneiro (Feb 11 2019 at 00:47):

it's not just about simp

Aymon Wuolanne (Feb 11 2019 at 00:51):

Also, out of curiosity what does rng/dom stand for?

Kenny Lau (Feb 11 2019 at 00:51):

range domain?

Mario Carneiro (Feb 11 2019 at 00:52):

rng is not a standard abbreviation, it should probably be renamed

Mario Carneiro (Feb 11 2019 at 00:53):

also neither of the two rng theorems mentions range

Mario Carneiro (Feb 11 2019 at 00:53):

I guess it should be cod instead (for codomain)


Last updated: Dec 20 2023 at 11:08 UTC