use dependent instance assumptions

Stream: general

[Miguel Marco]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Miguel Marco]

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

[Johan Commelin]

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