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

are 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 Y`

from `Y`

a 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: Dec 20 2023 at 11:08 UTC