Search results

feat(topology/final_topology): define final topology and universal pr…

new-contributorThis PR was made by a contributor with at most 5 merged PRs. Welcome to the community!This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 28232

#28232 In leanprover-community/mathlib4;

· nonisomorphiclinearmap opened on Aug 11, 2025

feat(Topology/ValuativeRel): continuous valuation when IsValuativeTopology

maintainer-merge

t-number-theoryNumber theory (also use t-algebra or t-analysis to specialize)Number theory (also use t-algebra or t-analysis to specialize)

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 28211

#28211 In leanprover-community/mathlib4;

· pechersky opened on Aug 11, 2025

feat(Topology): add the definition <code>foldTrans</code> to concatenate finite sequences of paths

blocked-by-other-PRThis PR depends on another PR (this label is automatically managed by a bot)This PR depends on another PR (this label is automatically managed by a bot)

new-contributorThis PR was made by a contributor with at most 5 merged PRs. Welcome to the community!This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 28208

#28208 In leanprover-community/mathlib4;

· Sebi-Kumar opened on Aug 10, 2025

feat(Topology/Homotopy/Path): Add IsEquiv instance for Path.Homotopic

new-contributorThis PR was made by a contributor with at most 5 merged PRs. Welcome to the community!This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 28186

#28186 In leanprover-community/mathlib4;

· Sebi-Kumar opened on Aug 10, 2025

feat(Topology/Path): add theorem about casting with rfl

new-contributorThis PR was made by a contributor with at most 5 merged PRs. Welcome to the community!This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 28185

#28185 In leanprover-community/mathlib4;

· Sebi-Kumar opened on Aug 10, 2025

feat: hensel's lemma for topological rings

t-algebraAlgebra (groups, rings, fields, etc)Algebra (groups, rings, fields, etc)

t-ring-theoryRing theoryRing theory

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

WIPWork in progressWork in progress

Status: Draft (not ready).

leanprover-community/mathlib4number 28168

#28168 In leanprover-community/mathlib4;

· astrainfinita opened on Aug 10, 2025

feat: nontriviality of <code>SeparationQuotient</code> iff the topology is nontrivial

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 28102

#28102 In leanprover-community/mathlib4;

· eric-wieser opened on Aug 8, 2025

Feat(Topology/ContinuousMap/Lattice): add instance <code>IsOrderedAddMonoid</code>

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 27994

#27994 In leanprover-community/mathlib4;

· yoh-tanimoto opened on Aug 5, 2025

refactor: have <code>MetrizableSpace</code> not depend on <code>MetricSpace</code>

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 27946

#27946 In leanprover-community/mathlib4;

· plp127 opened on Aug 4, 2025

feat(Topology/Algebra/InfiniteSum/NatInt): add more pnat tsum lemmas

help-wantedThe author needs attention to resolve issuesThe author needs attention to resolve issues

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 27841

#27841 In leanprover-community/mathlib4;

· CBirkbeck opened on Aug 1, 2025

feat(Topology): <code>IsDenseInducing.isUniformInducing_extend</code>

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

Status: Open (in progress).

leanprover-community/mathlib4number 27790

#27790 In leanprover-community/mathlib4;

· pechersky opened on Jul 31, 2025

feat: <code>Weak(Pseudo)EMetricSpace</code>, generalises <code>(Pseudo)EMetricSpace</code>

carlesonpart of the ongoing formalization of Carleson's theorempart of the ongoing formalization of Carleson's theorem

t-topologyTopological spaces, uniform spaces, metric spaces, filtersTopological spaces, uniform spaces, metric spaces, filters

WIPWork in progressWork in progress

Status: Open (in progress).

leanprover-community/mathlib4number 27756

#27756 In leanprover-community/mathlib4;

· grunweg opened on Jul 31, 2025