## Stream: new members

### Topic: Declaring number of elements in a Topological Space

#### Suryansh Shrivastava (Oct 12 2023 at 01:02):

We know that Finite Particular Point Topology is a general case of Sierpinski space when the no. of points in the topological space. How does one define that there exists these particular amount of elements of that type

#### Luigi Massacci (Oct 12 2023 at 11:22):

You may want to wait for an answer from someone more authoritative, but I think you can just use Fin n (where n is the number of elements)

#### Eric Rodriguez (Oct 12 2023 at 12:59):

Yes, I'm not familiar with the area but I'd recommend defining something like def SierpinskiSpace (n : Nat) := Fin n and then create the topology on such a clone, as I think they may already have some topology by "accident" and I doubt it will be the one you want.

#### Eric Rodriguez (Oct 12 2023 at 12:59):

To define a topology, you will need to make a docs#TopologicalSpace instance.

#### Eric Rodriguez (Oct 12 2023 at 13:00):

Indeed there is, docs#instTopologicalSpaceFin gives it the discrete topology.

#### Eric Rodriguez (Oct 12 2023 at 13:01):

In fact, with some details I see that this can be defined for all spaces, not just finite ones. I'd instead recommend defining def ParticularPointTopology (X : Type*) := X and create your topological space instance on there. I'm not sure if I'm being very clear, feel free to ask any questions you have!

#### Riccardo Brasca (Oct 12 2023 at 14:01):

You also need to choose a point, right? I mean, mathematically

#### Suryansh Shrivastava (Oct 12 2023 at 22:11):

Also, if I am declaring a space to be uncountable, how does one pick an element from that space

#### Yaël Dillies (Oct 12 2023 at 22:11):

docs#Classical.arbitrary

#### Suryansh Shrivastava (Nov 02 2023 at 18:08):

Also, if I need to pick 2 distinct elements, what can I do?

#### Alex J. Best (Nov 02 2023 at 18:12):

If you only want two you can use docs#exists_pair_ne

#### Suryansh Shrivastava (Nov 02 2023 at 18:25):

How does one prove something like

variable [Fintype α ](hn : n = Fintype.card α )(hn1 : n > 2)

instance Nonempty_α : Nonempty α := by

sorry


#### Ruben Van de Velde (Nov 02 2023 at 18:28):

import Mathlib
variable [Fintype α ](hn : n = Fintype.card α )(hn1 : n > 2)

instance Nonempty_α : Nonempty α := by
subst hn
refine Fintype.card_pos_iff.mp ?_ -- first hit from apply?
linarith


Last updated: Dec 20 2023 at 11:08 UTC