General topology

Point-set topology of topological and metric spaces: connectedness, separation and cardinal invariants, homogeneous spaces, direct and inverse limits of spaces, restricted products, and dimension theory.

TheoremA preconnected set meets the frontier of every set it crosses#✓fully proved

Let \(s\) be a preconnected subset of a topological space \(X\) and let \(A \subseteq X\). If both \(s \cap A\) and \(s \cap (X \setminus A)\) are nonempty, then \(s\) meets the frontier \(\partial A = \overline{A} \setminus \operatorname{int} A\) of \(A\), that is, \(s \cap \partial A\) is nonempty.

theorem IsPreconnected.inter_frontier_nonempty_of_inter_compl {s : Set α}
    (hs : IsPreconnected s) {A : Set α} (hA : (s ∩ A).Nonempty)
    (hAc : (s ∩ Aᶜ).Nonempty) : (s ∩ frontier A).Nonempty

Used by 1

Used byBoundary cubes meet the dilated frontier charts

TheoremBounded metric \(d/(1+d)\) is equivalent to \(d\)#●ready to prove

Let \((X,d)\) be a metric space and define

[ \delta(x,y):=\frac{d(x,y)}{1+d(x,y)}, \qquad x,y\in X. ] Prove that \(d\) and \(\delta\) are equivalent metrics on \(X\).

Lean variant: the source statement asserts only that d-balls and δ-balls are mutually nested, which omits the claim that δ is a metric; the metric axioms of δ are added as a first conjunct.

public theorem_wanted dist_div_one_add_dist_balls_equivalent {X : Type*} [MetricSpace X]
    (δ : X → X → ℝ) (hδ : ∀ x y : X, δ x y = dist x y / (1 + dist x y)) :
    ((∀ x y : X, δ x y = 0 ↔ x = y) ∧ (∀ x y : X, δ x y = δ y x) ∧
      (∀ x y z : X, δ x z ≤ δ x y + δ y z)) ∧
    (∀ x : X, ∀ ε > 0, ∃ η > 0, Metric.ball x η ⊆ {y : X | δ x y < ε}) ∧
    (∀ x : X, ∀ ε > 0, ∃ η > 0, {y : X | δ x y < η} ⊆ Metric.ball x ε)

Sources

MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Inequalities in real analysis), problem ma_proofbench_l1_65, with the change above.

ClassHomogeneous topological space#✓fully proved

A topological space is homogeneous if its homeomorphism group acts transitively.

class HomogeneousSpace (X : Type*) [TopologicalSpace X] : Prop where
  is_transitive : ∀ x y : X, ∃ f : Homeomorph X X, f x = y

TheoremKrull dimension drops on proper closed subsets of irreducible sets#✓fully proved

A proper closed subset of an irreducible set has Krull dimension at least one less than the ambient set.

theorem IsIrreducible.topologicalKrullDim_add_one_le_of_isClosed_of_ne
    {X : Type u} [TopologicalSpace X] {Y Z : Set X}
    (hZ : IsIrreducible Z) (hY : IsClosed Y) (hYZ : Y ⊆ Z) (hne : Y ≠ Z) :
    topologicalKrullDim Y + 1 ≤ topologicalKrullDim Z

TheoremKuratowski's closure-complement theorem#✓fully proved

Let \(X\) be a topological space and \(s \subseteq X\). The sets that can be obtained from \(s\) by applying closure and complement finitely many times (including \(s\) itself) form a finite family of at most \(14\) distinct sets.

theorem kuratowski_closure_complement (s : Set X) :
    {t : Set X | Topology.ClosureCompl.IsObtainable s t}.Finite ∧
      {t : Set X | Topology.ClosureCompl.IsObtainable s t}.ncard ≤ 14

Sources

Casimir Kuratowski, "Sur l'opération Ā de l'Analysis Situs," Fundamenta Mathematicae 3 (1922), 182–199, DOI 10.4064/FM-3-1-182-199.

DefinitionNon-strictly separated sets#✓fully proved

Let \(X\) be a pseudo-extended metric space (distances lie in \([0, \infty]\) and distinct points may be at distance \(0\)), write \(d\) for its extended distance, and let \(\varepsilon \in [0, \infty]\). A set \(s \subseteq X\) is \(\varepsilon\)-separated if \(\varepsilon \le d(x, y)\) for all distinct points \(x, y \in s\).

def IsSeparated' (ε : ℝ≥0∞) (s : Set X) : Prop := s.Pairwise (ε ≤ edist · ·)

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.