search

pi-base / data

A community database of topological counterexamples
https://topology.pi-base.org/
Creative Commons Attribution 4.0 International
72 stars 26 forks source link

Property Suggestion: Has a closed point #940

Open GeoffreySangston opened 4 days ago

GeoffreySangston commented 4 days ago

Property Suggestion

'Has a closed point': Some singleton $\{x\}$ of the space is closed.

Rationale

This seems like a convenient and easily recognizable utility property. The concept of a closed point is common; e.g., in a common definition of T1 space.

Compare with Has an isolated point (P139).

Relationship to other properties

  1. 'Has a closed point' implies ~Empty (P137)
  2. $T_1$ (P002) + ~Empty (P137) implies Has a closed point
  3. Has a cut point (P204) + ~Has an isolated point (P139) implies Has a closed point
  4. Ultraconnected (P040) + Has a cut point (P204) implies Has a closed point
  5. Ultraconnected + Has a closed point implies Has a focal point
  6. Homogeneous (P086) + Has a closed point implies $T_1$ (P002).

(I won't try to exhaust the entire list. Surely there are many others, and feel free to edit it any that you see. Hopefully this is enough to begin the discussion though.)

Other remarks

prabau commented 4 days ago

Yeah, I have often thought this would be a nice thing to have.

@StevenClontz Would you agree?

prabau commented 4 days ago

I particularly like the relationship (5) that is the dual of: T597: Hyperconnected + Has an isolated point ==> Has a generic point.

Almanzoris commented 3 days ago

@GeoffreySangston I have read your suggestion again and I agree on incorporating the property and the results.

I wanted to prove the theorems of the list before saying anything here, and last night was already certainly late.

prabau commented 3 days ago

I would imagine several of the existing theorems will also be able to be strengthened or simplified using the new notion, or replaced by one of the suggested theorems above.

StevenClontz commented 20 hours ago

Yeah, I have often thought this would be a nice thing to have.

@StevenClontz Would you agree?

Seems reasonable to me at a glance. I'd like to see the PR that introduces it to demonstrate its utility: define the property, add whatever theorems seem most useful/obvious, and clean up traits for one (not all!) space using those new theorems.