Declaring number of elements in a Topological Space

Stream: new members

[Suryansh Shrivastava]

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]

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]

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]

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

[Eric Rodriguez]

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

[Eric Rodriguez]

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]

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

[Suryansh Shrivastava]

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

[Yaël Dillies]

docs#Classical.arbitrary

[Suryansh Shrivastava]

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

[Alex J. Best]

If you only want two you can use docs#exists_pair_ne

[Suryansh Shrivastava]

How does one prove something like

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

instance Nonempty_α : Nonempty α := by

  sorry

[Ruben Van de Velde]

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