Locally orderable spaces are radial

[prabau]

New theorem: Locally orderable => radial.

Plus some metaproperties for Radial. I added "not preserved by products" because it was not initially obvious, and could be surprising to some.

This theorem allows to derive two more spaces are radial: S40 (altered long ray) and S196 (long circle),
and two more spaces are not locally orderable: S109 (Novak space) and S110 (strong ultrafilter topology).

[prabau]

One could shorten the proof of the thm by just saying Radial is a "local property" (which is being proved as part of the theorem here) and using LOTS => radial. I just went with this longer way.

[yhx-12243]

Looks T774~T777 seem to be preserved by #1426?

[prabau]

good point. I'll change the number.

[prabau]

The metaprop that Radial (P172) is a "local property" is simple enough, so there should be no need to justify it with a mathse post or a reference to some book/paper.

Based on that, one could just shorten the justification of the theorem to the following:

This follows from the fact that {P172} is a "local" property,
and {P133} spaces are {P172}
[(Explore)](https://topology.pi-base.org/spaces?q=LOTS%2B%7ERadial).

Would that be preferable?

[Moniker1998]

@prabau to me, yes

[Moniker1998]

@prabau actually, why the quotation marks?

[prabau]

because we have not defined what it means. It could mean different things in general. In this case, it's referring to what is spelled out as one of the meta-properties, but I did not feel like repeating all that. If that's too terse, we may as well give more details about the proof.

Note: @StevenClontz has suggested that in the future there will be some kind of dictionary of often used terms in pi-base. If that happens, we can better define what we mean and have links to suitable definitions.

[felixpernegger]

A property being "local" is a well defined notion (at least in Algebra(ic Geometry) and apparently also in topology), so the quotes are not necessary.

A rather rudimentary formalisation of this in Lean would be

def IsLocal.{u} (P : (X : Type u) → TopologicalSpace X → Prop) : Prop :=
  ∀ (X : Type u) [i : TopologicalSpace X], P X i ↔ ∀ x : X, ∃ s ∈ 𝓝 x, P s instTopologicalSpaceSubtype

:)

[yhx-12243]

π-base wiki Conventions and Style has already specify how local properties means.

[felixpernegger]

π-base wiki Conventions and Style has already specify how local properties means.

Technically this only says given a property P, what (weakly) locally P means, but not the notion of a property being (weakly) local. Probably should be added.

[felixpernegger]

Having: "This property is (weakly?) local." might be useful as a metaproperty in general actually