universal properties for topology

Stream: new members

[Aymon Wuolanne]

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]

I think it's already there

[Kenny Lau]

something about induced / coinduced topology

[Reid Barton]

It's also embedding.continuous_iff plus embedding_subtype_val

[Mario Carneiro]

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

[Mario Carneiro]

or embedding_subtype_val

[Kenny Lau]

continuous_induced_rng?

[Mario Carneiro]

yes, but it needs restatement

[Mario Carneiro]

also couldn't that theorem be an iff?

[Aymon Wuolanne]

Ah yep, I think continuous_induced_rng works well enough

[Aymon Wuolanne]

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

[Kenny Lau]

you simp-minded people /s

[Mario Carneiro]

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

[Mario Carneiro]

it's not just about simp

[Aymon Wuolanne]

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

[Kenny Lau]

range domain?

[Mario Carneiro]

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

[Mario Carneiro]

also neither of the two rng theorems mentions range

[Mario Carneiro]

I guess it should be cod instead (for codomain)