Zulip Chat Archive

Stream: new members

Topic: Curiosity about class instances in mathlib docs

Pedro Minicz (Oct 05 2020 at 13:06):

Shouldn't [topological_space (subtype p)] be required by this definition?

Pedro Minicz (Oct 05 2020 at 13:07):

I am not with Lean right now, but I feel like it should be in the context, otherwise how would is be able to make sense of is_closed for subtype p?

Heather Macbeth (Oct 05 2020 at 13:07):

I believe it's inferred automatically, docs#subtype.topological_space

Pedro Minicz (Oct 05 2020 at 13:08):

Definition is here. It may also be just that the docs aren't showing the instance.

Pedro Minicz (Oct 05 2020 at 13:09):

Yes, it should be inferred automatically. Therefore it should be included in the type full type signature as a hidden argument, right?

Heather Macbeth (Oct 05 2020 at 13:10):

Rather, I believe the classes that appear in the full type signature are those that are not inferred automatically.

Johan Commelin (Oct 05 2020 at 13:11):

@Pedro Minicz Luckily not... otherwise everything that uses a little bit of ring theory would show an insane amount of type class arguments.

Pedro Minicz (Oct 05 2020 at 13:12):


Pedro Minicz (Oct 05 2020 at 13:13):

It makes sense. That had never occurred to me.

Yury G. Kudryashov (Oct 05 2020 at 13:29):

This lemma doesn't take an instance of [topological_space (subtype p)] with some unknown properties. Instead, there is subtype.topological_space hidden in the implicit arguments of t1_space (subtype p). Actually, it is something like @t1_space (subtype p) (@subtype.topological_space α p t), where [t : topological_space α].

Last updated: Dec 20 2023 at 11:08 UTC