leanprover-community/mathlib4

Define a typeclass for GO-space

Ouverte

#42 275 ouverte le 30 juil. 2026

Voir sur GitHubGuide contributeur
 (0 commentaire) (0 réaction) (0 personne assignée)Lean (1 549 forks)github user discovery
good first issuet-topology

Métriques du dépôt

Stars
 (3 755 étoiles)
Métriques de merge PR
 (Aucune PR mergée en 30 j)

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.

Guide contributeur

Direction de recherche
Étudiez la définition de GO space à partir du lien fourni, examinez les modèles de classes de types et de théorèmes dans mathlib pour les propriétés topologiques, et consultez la PR #41918 pour le contexte et l'approche possible.
Stack technique
Aucun
Domaine
Aucun
Type d'issue
Fonctionnalité
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-2 jours
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Récente
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
GitLean 4Basic topology
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
30