leanprover-community/mathlib4

Define a typeclass for GO-space

Aberta

#42.275 aberto em 30 de jul. de 2026

Ver no GitHubGuia do colaborador
 (1 comentário) (1 reação) (0 responsável)Lean (1.592 forks)github user discovery
good first issuet-topology

Métricas do repositório

Stars
 (3.869 estrelas)
Métricas de merge de PR
 (Nenhuma PRs mesclada em 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.

Guia do colaborador

Direção de pesquisa
Estude a definição de GO space no link fornecido, examine os padrões de typeclass e teoremas no mathlib para propriedades topológicas e revise a PR #41918 para contexto e possível abordagem.
Pilha de tecnologia
None
Domain
None
Tipo Issue
Funcionalidade
DifficultyDificuldade de implementação estimada para um novo contribuidor, de 1 para alterações muito pequenas a 5 para trabalho de nível especializado.
3
Tempo estimadoUm intervalo de tempo aproximado para um colaborador experiente investigar, implementar, testar e preparar um pull request.
1-2 dias
Status da atividadeQuão disponível o issue aparece agora: novo, ativo, obsoleto, bloqueado ou aguardando entrada do mantenedor.
Recente
ClarityCom que clareza o issue explica a mudança esperada, os critérios de aceitação e a próxima etapa.
Claro
Prerequisites
GitLean 4Basic topology
Simpatia para novatosUma pontuação de 1 a 100 que estima o quão acessível este issue é para colaboradores iniciantes.
30