leanprover-community/mathlib4

Define a typeclass for GO-space

Aperta

#42.275 aperta il 30 lug 2026

Vedi su GitHubGuida contributor
 (1 commento) (1 reazione) (0 assegnatari)Lean (1592 fork)github user discovery
good first issuet-topology

Metriche repository

Star
 (3869 stelle)
Metriche merge PR
 (Nessuna PR mergiata in 30 g)

Descrizione

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.

Guida contributor

Direzione di ricerca
Studia la definizione di GO space dal link fornito, esamina i pattern di typeclass e teoremi in mathlib per le proprietà topologiche e rivedi la PR #41918 per contesto e possibili approcci.
Tech stack
Nessuno
Dominio
Nessuno
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Nuova
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
GitLean 4Basic topology
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
30