## 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