Zulip Chat Archive

Stream: general

Topic: use dependent instance assumptions

Miguel Marco (May 11 2022 at 16:17):

I am preparing material for a topology course using lean and I am now trying to prove that a function between a topological space X (with an arbritrary topology) and a space Y with the topology generated by a set of sets S is continuous, iff the preimages of the elements of Sare open.

I want to do everything in my course from the basics, so i am ignoring the topology part of mathlib (will use stuff about sets and functions though).

So I have the class topological_space, the definition of continous for functions, which requires both types to be topological space, and
a function generated_topology, which returns something of the type topological space Yfrom Ya and S.

Now, if i want to write my theorem

theorem continuous_on_generated {X Y : Type} { S : set (set Y)} [hTX :topological_space X]  [hTY : generated_topology Y S] (f : X  Y):
continua f   s  S, (open (f ⁻¹' s))

I get the error message

type expected at
 generated_topology Y S
term has type
  topological_space Y

Is there a way to introduce an assumption that consist on a class instance, but depends on other items of the input (in this case, the fact that Y is not just a generic topological space, but that it has that specific topology).

Johan Commelin (May 11 2022 at 16:24):

What you want to do is pass generated_topology Y S into continuous f as the topology on Y.

Johan Commelin (May 11 2022 at 16:25):

So you shouldn't write [hTY : generated_topology Y S], because that means you are trying to assume a term of type generated_topology Y S, but it isn't a type, it's a term of topological_space Y.

Johan Commelin (May 11 2022 at 16:25):

Instead, write @continuous X Y _ (generated_topology Y S) f.

Johan Commelin (May 11 2022 at 16:26):

Here, I am guess the order of the arguments. Maybe it should be X _ Y instead of X Y _.

Miguel Marco (May 11 2022 at 16:31):

I see, so the @ in continuous means "don't try to infer class instances, but use this explicit ones".

Johan Commelin (May 11 2022 at 16:34):

Roughly, yes. Although the _ still causes Lean to infer the topology on X by itself.

Last updated: Aug 03 2023 at 10:10 UTC