leanprover-community/mathlib4

Define a typeclass for GO-space

Offen

#42.275 geöffnet am 30.07.2026

Auf GitHub ansehenContributor Guide
 (1 Kommentar) (1 Reaktion) (0 zugewiesene Personen)Lean (1.592 Forks)github user discovery
good first issuet-topology

Repository-Metriken

Stars
 (3.869 Sterne)
PR-Merge-Metriken
 (Keine gemergten PRs in 30 T)

Beschreibung

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-Richtung
Studieren Sie die Definition von GO Raum aus dem bereitgestellten Link, untersuchen Sie die Muster von Typklassen und Theoremen in mathlib für topologische Eigenschaften und prüfen Sie die PR #41918 für Kontext und mögliche Ansätze.
Tech Stack
Keine
Domain
Keine
Issue Type
Funktion
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
3
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
1-2 Tage
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Frisch
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
GitLean 4Basic topology
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
30