good first issuet-topology
Repository metrics
- Stars
- (3,869 個のスター)
- PR merge metrics
- (30d に merged PR はありません)
説明
The definition of a GO-space can be found here: https://topology.pi-base.org/properties/P000154
Also prove the following lemmas:
- A linearly ordered space is a GO-space.
- A separable GO-space is hereditarily separable.
- Optional: other lemmas that you can find on https://topology.pi-base.org/properties/P000154.
This is mentioned in https://github.com/leanprover-community/mathlib4/pull/41918.