leanprover-community/mathlib4

Define a typeclass for GO-space

Open

#42,275 opened on Jul 30, 2026

View on GitHubContributor guide
 (0 comments) (0 reactions) (0 assignees)Lean (1,549 forks)github user discovery
good first issuet-topology

Repository metrics

Stars
 (3,755 stars)
PR merge metrics
 (No merged PRs in 30d)

Description

The definition of a GO-space can be found here: https://topology.pi-base.org/properties/P000154

Also prove the following lemmas:

  1. A linearly ordered space is a GO-space.
  2. A separable GO-space is hereditarily separable.
  3. 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.

Contributor guide

Research direction
Study the definition of GO space from the provided link, examine existing typeclass and theorem patterns in mathlib for topological properties, and review the referenced PR #41918 for context and potential approach.
Tech stack
None
Domain
None
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-2 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Fresh
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
GitLean 4Basic topology
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
30