Skip to content

Commit 5210a06

Browse files
joelriouReemMelamed
joelriou
authored and
ReemMelamed
committed
refactor(Topology): redefine Delta-generated spaces (leanprover-community#38431)
Delta-generated spaces are made particular cases of `X`-generated spaces, where `X` is the family of spaces `Fin n → ℝ`.
1 parent ccfb2f8 commit 5210a06

4 files changed

Lines changed: 144 additions & 211 deletions

File tree

‎Mathlib/Topology/Category/DeltaGenerated.lean‎

Lines changed: 27 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,30 @@
11
/-
22
Copyright (c) 2024 Ben Eltschig. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Ben Eltschig
4+
Authors: Ben Eltschig, Joël Riou
55
-/
66
module
77

88
public import Mathlib.CategoryTheory.Monad.Limits
99
public import Mathlib.Topology.Category.TopCat.Limits.Basic
1010
public import Mathlib.Topology.Compactness.DeltaGeneratedSpace
11+
public import Mathlib.Topology.Convenient.Category
1112

1213
/-!
1314
# Delta-generated topological spaces
1415
15-
The category of delta-generated spaces.
16+
This file defines the category `DeltaGenerated` of delta-generated spaces.
17+
This is a particular case of the construction in the file
18+
`Mathlib/Topology/Convenient/Category.Lean`: this is the category of
19+
`X`-generated spaces where `X` is the family of spaces `Fin n → ℝ`
20+
for all `n : ℕ`.
1621
17-
See https://ncatlab.org/nlab/show/Delta-generated+topological+space.
22+
## TODO
23+
* `DeltaGenerated` is Cartesian closed (@joelriou).
1824
19-
Adapted from `Mathlib/Topology/Category/CompactlyGenerated.lean`.
25+
## References
26+
* https://ncatlab.org/nlab/show/Delta-generated+topological+space
2027
21-
## TODO
22-
* `DeltaGenerated` is Cartesian closed.
2328
-/
2429

2530
@[expose] public section
@@ -28,77 +33,32 @@ universe u
2833

2934
open CategoryTheory
3035

31-
/-- The type of delta-generated topological spaces. -/
32-
structure DeltaGenerated where
33-
/-- the underlying topological space -/
34-
toTop : TopCat.{u}
35-
/-- The underlying topological space is delta-generated. -/
36-
deltaGenerated : DeltaGeneratedSpace toTop := by infer_instance
37-
38-
namespace DeltaGenerated
36+
/-- The category of delta-generated topological spaces. -/
37+
abbrev DeltaGenerated := GeneratedByTopCat.{u} (fun n ↦ Fin n → ℝ)
3938

40-
instance : CoeSort DeltaGenerated Type* :=
41-
⟨fun X ↦ X.toTop⟩
42-
43-
attribute [instance] deltaGenerated
44-
45-
instance : LargeCategory.{u} DeltaGenerated.{u} :=
46-
inferInstanceAs <| Category (InducedCategory _ toTop)
39+
/-- The faithful (but not full) functor taking each topological space to its delta-generated
40+
coreflection. -/
41+
abbrev TopCat.toDeltaGenerated : TopCat.{u} ⥤ DeltaGenerated.{u} :=
42+
TopCat.toGeneratedByTopCat
4743

48-
instance : ConcreteCategory.{u} DeltaGenerated.{u} (C(·, ·)) :=
49-
inferInstanceAs <| ConcreteCategory (InducedCategory _ toTop) _
44+
namespace DeltaGenerated
5045

5146
/-- Constructor for objects of the category `DeltaGenerated` -/
52-
abbrev of (X : Type u) [TopologicalSpace X] [DeltaGeneratedSpace X] : DeltaGenerated.{u} where
53-
toTop := TopCat.of X
54-
deltaGenerated := ‹_›
47+
abbrev of (X : Type u) [TopologicalSpace X] [DeltaGeneratedSpace X] : DeltaGenerated.{u} :=
48+
GeneratedByTopCat.of X
5549

5650
/-- The forgetful functor `DeltaGenerated ⥤ TopCat` -/
57-
@[simps!]
58-
def deltaGeneratedToTop : DeltaGenerated.{u} ⥤ TopCat.{u} :=
59-
inducedFunctor _
51+
abbrev deltaGeneratedToTop : DeltaGenerated.{u} ⥤ TopCat.{u} :=
52+
GeneratedByTopCat.toTopCat
6053

6154
/-- `deltaGeneratedToTop` is fully faithful. -/
62-
def fullyFaithfulDeltaGeneratedToTop : deltaGeneratedToTop.{u}.FullyFaithful :=
63-
fullyFaithfulInducedFunctor _
64-
65-
instance : deltaGeneratedToTop.{u}.Full := fullyFaithfulDeltaGeneratedToTop.full
66-
67-
instance : deltaGeneratedToTop.{u}.Faithful := fullyFaithfulDeltaGeneratedToTop.faithful
68-
69-
/-- The faithful (but not full) functor taking each topological space to its delta-generated
70-
coreflection. -/
71-
@[simps!]
72-
def topToDeltaGenerated : TopCat.{u} ⥤ DeltaGenerated.{u} where
73-
obj X := of (DeltaGeneratedSpace.of X)
74-
map {_ Y} f := ConcreteCategory.ofHom ⟨f, (continuous_to_deltaGenerated (Y := Y)).mpr <|
75-
continuous_le_dom deltaGenerated_le f.hom.continuous⟩
55+
abbrev fullyFaithfulDeltaGeneratedToTop : deltaGeneratedToTop.{u}.FullyFaithful :=
56+
GeneratedByTopCat.fullyFaithfulToTopCat _
7657

77-
instance : topToDeltaGenerated.{u}.Faithful :=
78-
⟨fun h ↦ by ext x; exact CategoryTheory.congr_fun h x⟩
58+
@[deprecated (since := "2026-04-23")] alias topToDeltaGenerated := TopCat.toDeltaGenerated
7959

8060
/-- The adjunction between the forgetful functor `DeltaGenerated ⥤ TopCat` and its coreflector. -/
81-
def coreflectorAdjunction : deltaGeneratedToTop ⊣ topToDeltaGenerated :=
82-
Adjunction.mkOfUnitCounit {
83-
unit := {
84-
app X := ConcreteCategory.ofHom
85-
⟨id, continuous_iff_coinduced_le.mpr (eq_deltaGenerated (X := X)).le⟩ }
86-
counit := {
87-
app X := ConcreteCategory.ofHom
88-
⟨DeltaGeneratedSpace.counit, DeltaGeneratedSpace.continuous_counit⟩ } }
89-
90-
/-- The category of delta-generated spaces is coreflective in the category of topological spaces. -/
91-
instance deltaGeneratedToTop.coreflective : Coreflective deltaGeneratedToTop where
92-
R := topToDeltaGenerated
93-
adj := coreflectorAdjunction
94-
95-
noncomputable instance deltaGeneratedToTop.createsColimits : CreatesColimits deltaGeneratedToTop :=
96-
comonadicCreatesColimits deltaGeneratedToTop
97-
98-
instance hasLimits : Limits.HasLimits DeltaGenerated :=
99-
hasLimits_of_coreflective deltaGeneratedToTop
100-
101-
instance hasColimits : Limits.HasColimits DeltaGenerated :=
102-
hasColimits_of_hasColimits_createsColimits deltaGeneratedToTop
61+
abbrev coreflectorAdjunction : deltaGeneratedToTop ⊣ TopCat.toDeltaGenerated :=
62+
GeneratedByTopCat.adj
10363

10464
end DeltaGenerated

‎Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean‎

Lines changed: 83 additions & 141 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
11
/-
22
Copyright (c) 2024 Ben Eltschig. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Ben Eltschig
4+
Authors: Ben Eltschig, Joël Riou
55
-/
66
module
77

8+
public import Mathlib.Topology.Convenient.GeneratedBy
89
public import Mathlib.Analysis.LocallyConvex.WithSeminorms
910

1011
/-!
@@ -17,7 +18,11 @@ locally path-connected, sequential and in particular compactly generated.
1718
1819
See https://ncatlab.org/nlab/show/Delta-generated+topological+space.
1920
20-
Adapted from `Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean`.
21+
The notions defined in this file (see also the file
22+
`Mathlib/Topology/Category/DeltaGenerated.lean` for the category `DeltaGenerated`)
23+
are a particular case of the notion of `X`-generated topological spaces where
24+
`X` is a family of topological spaces (see the file
25+
`Mathlib/Topology/Convenient/GeneratedBy.lean`.)
2126
2227
## TODO
2328
* All locally path-connected first-countable spaces are delta-generated - in particular, all normed
@@ -28,158 +33,95 @@ Adapted from `Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean`.
2833

2934
@[expose] public section
3035

31-
variable {X Y : Type*} [tX : TopologicalSpace X] [tY : TopologicalSpace Y]
32-
3336
open TopologicalSpace Topology
3437

38+
/-- A topological space is Delta-generated if its topology is generated
39+
by the continuous maps from topological spaces of the form `Fin n → ℝ`. -/
40+
abbrev DeltaGeneratedSpace (Y : Type*) [TopologicalSpace Y] : Prop :=
41+
IsGeneratedBy (fun n ↦ Fin n → ℝ) Y
42+
43+
namespace DeltaGeneratedSpace
44+
45+
variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
46+
47+
/-- Type synonym to be equipped with the delta-generated topology. -/
48+
abbrev of : Type _ := WithGeneratedByTopology (fun n ↦ Fin n → ℝ) Y
49+
50+
/-- Delta-generated spaces are locally path-connected. -/
51+
instance [DeltaGeneratedSpace X] :
52+
LocPathConnectedSpace X := by
53+
rw [← IsGeneratedBy.generatedBy_eq (X := fun n ↦ Fin n → ℝ) (Y := X),
54+
generatedBy_eq_coinduced]
55+
exact LocPathConnectedSpace.coinduced _
56+
57+
/-- Delta-generated spaces are sequential. -/
58+
instance [DeltaGeneratedSpace X] : SequentialSpace X := by
59+
rw [← IsGeneratedBy.generatedBy_eq (X := fun n ↦ Fin n → ℝ) (Y := X)]
60+
exact SequentialSpace.iSup (fun n ↦ SequentialSpace.iSup
61+
(fun f ↦ SequentialSpace.coinduced _))
62+
63+
end DeltaGeneratedSpace
64+
3565
/-- The topology coinduced by all maps from ℝⁿ into a space. -/
36-
@[implicit_reducible]
66+
@[implicit_reducible, deprecated "Use TopologicalSpace.generatedBy" (since := "2026-04-23")]
3767
def TopologicalSpace.deltaGenerated (X : Type*) [TopologicalSpace X] : TopologicalSpace X :=
3868
⨆ f : (n : ℕ) × C(((Fin n) → ℝ), X), coinduced f.2 inferInstance
3969

40-
/-- The delta-generated topology is also coinduced by a single map out of a sigma type. -/
41-
lemma deltaGenerated_eq_coinduced : deltaGenerated X = coinduced
42-
(fun x : (f : (n : ℕ) × C(Fin n → ℝ, X)) × (Fin f.1 → ℝ) ↦ x.1.2 x.2) inferInstance := by
43-
rw [deltaGenerated, instTopologicalSpaceSigma, coinduced_iSup]; rfl
44-
45-
/-- The delta-generated topology is at least as fine as the original one. -/
46-
lemma deltaGenerated_le : deltaGenerated X ≤ tX :=
47-
iSup_le_iff.mpr fun f ↦ f.2.continuous.coinduced_le
48-
49-
/-- A set is open in `deltaGenerated X` iff all its preimages under continuous functions ℝⁿ → X are
50-
open. -/
51-
lemma isOpen_deltaGenerated_iff {u : Set X} :
52-
IsOpen[deltaGenerated X] u ↔ ∀ n (p : C(Fin n → ℝ, X)), IsOpen (p ⁻¹' u) := by
53-
simp_rw +instances [deltaGenerated, isOpen_iSup_iff, isOpen_coinduced, Sigma.forall]
54-
55-
/-- A map from ℝⁿ to X is continuous iff it is continuous regarding the
56-
delta-generated topology on X. Outside of this file, use the more general
57-
`continuous_to_deltaGenerated` instead. -/
58-
private lemma continuous_euclidean_to_deltaGenerated {n : ℕ} {f : (Fin n → ℝ) → X} :
59-
Continuous[_, deltaGenerated X] f ↔ Continuous f := by
60-
simp_rw [continuous_iff_coinduced_le]
61-
refine ⟨fun h ↦ h.trans deltaGenerated_le, fun h ↦ ?_⟩
62-
simp_rw [deltaGenerated]
63-
exact le_iSup_of_le (i := ⟨n, f, continuous_iff_coinduced_le.mpr h⟩) le_rfl
64-
65-
/-- `deltaGenerated` is idempotent as a function `TopologicalSpace X → TopologicalSpace X`. -/
66-
lemma deltaGenerated_deltaGenerated_eq :
67-
@deltaGenerated X (deltaGenerated X) = deltaGenerated X := by
68-
ext u; simp_rw [isOpen_deltaGenerated_iff]; refine forall_congr' fun n ↦ ?_
69-
-- somewhat awkward because `ContinuousMap` doesn't play well with multiple topologies.
70-
refine ⟨fun h p ↦ h <| @ContinuousMap.mk _ _ _ (_) p ?_, fun h p ↦ h ⟨p, ?_⟩⟩
71-
· exact continuous_euclidean_to_deltaGenerated.mpr p.2
72-
· exact continuous_euclidean_to_deltaGenerated.mp <| @ContinuousMap.continuous_toFun _ _ _ (_) p
73-
74-
/-- A space is delta-generated if its topology is equal to the delta-generated topology, i.e.
75-
coinduced by all continuous maps ℝⁿ → X. Since the delta-generated topology is always finer
76-
than the original one, it suffices to show that it is also coarser. -/
77-
class DeltaGeneratedSpace (X : Type*) [t : TopologicalSpace X] : Prop where
78-
le_deltaGenerated : t ≤ deltaGenerated X
79-
80-
lemma eq_deltaGenerated [DeltaGeneratedSpace X] : tX = deltaGenerated X :=
81-
eq_of_le_of_ge DeltaGeneratedSpace.le_deltaGenerated deltaGenerated_le
82-
83-
/-- A subset of a delta-generated space is open iff its preimage is open for every
84-
continuous map from ℝⁿ to X. -/
85-
lemma DeltaGeneratedSpace.isOpen_iff [DeltaGeneratedSpace X] {u : Set X} :
86-
IsOpen u ↔ ∀ (n : ℕ) (p : ContinuousMap ((Fin n) → ℝ) X), IsOpen (p ⁻¹' u) := by
87-
nth_rewrite 1 [eq_deltaGenerated (X := X)]; exact isOpen_deltaGenerated_iff
88-
89-
/-- A map out of a delta-generated space is continuous iff it preserves continuity of maps
90-
from ℝⁿ into X. -/
91-
lemma DeltaGeneratedSpace.continuous_iff [DeltaGeneratedSpace X] {f : X → Y} :
92-
Continuous f ↔ ∀ (n : ℕ) (p : C(((Fin n) → ℝ), X)), Continuous (f ∘ p) := by
93-
simp_rw [continuous_iff_coinduced_le]
94-
nth_rewrite 1 [eq_deltaGenerated (X := X), deltaGenerated]
95-
simp [coinduced_compose, Sigma.forall]
96-
97-
/-- A map out of a delta-generated space is continuous iff it is continuous with respect
98-
to the delta-generated topology on the codomain. -/
99-
lemma continuous_to_deltaGenerated [DeltaGeneratedSpace X] {f : X → Y} :
100-
Continuous[_, deltaGenerated Y] f ↔ Continuous f := by
101-
simp_rw [DeltaGeneratedSpace.continuous_iff, continuous_euclidean_to_deltaGenerated]
102-
103-
/-- The delta-generated topology on `X` does in fact turn `X` into a delta-generated space. -/
104-
lemma deltaGeneratedSpace_deltaGenerated {X : Type*} {t : TopologicalSpace X} :
105-
@DeltaGeneratedSpace X (@deltaGenerated X t) := by
106-
let _ := @deltaGenerated X t; constructor; rw [@deltaGenerated_deltaGenerated_eq X t]
107-
108-
lemma deltaGenerated_mono {X : Type*} {t₁ t₂ : TopologicalSpace X} (h : t₁ ≤ t₂) :
109-
@deltaGenerated X t₁ ≤ @deltaGenerated X t₂ := by
110-
rw [← continuous_id_iff_le, @continuous_to_deltaGenerated _ _
111-
(@deltaGenerated X t₁) t₂ deltaGeneratedSpace_deltaGenerated id]
112-
exact continuous_id_iff_le.2 <| (@deltaGenerated_le X t₁).trans h
70+
@[deprecated (since := "2026-04-23")]
71+
alias deltaGenerated_eq_coinduced := generatedBy_eq_coinduced
11372

114-
namespace DeltaGeneratedSpace
73+
@[deprecated (since := "2026-04-23")] alias deltaGenerated_le := generatedBy_le
11574

116-
/-- Type synonym to be equipped with the delta-generated topology. -/
117-
def of (X : Type*) := X
75+
@[deprecated (since := "2026-04-23")]
76+
alias isOpen_deltaGenerated_iff := WithGeneratedByTopology.isOpen_iff
11877

119-
instance : TopologicalSpace (of X) := deltaGenerated X
78+
@[deprecated (since := "2026-04-23")]
79+
alias deltaGenerated_deltaGenerated_eq := generatedBy_generatedBy
12080

121-
instance : DeltaGeneratedSpace (of X) :=
122-
deltaGeneratedSpace_deltaGenerated
81+
@[deprecated (since := "2026-04-23")]
82+
alias eq_deltaGenerated := IsGeneratedBy.generatedBy_eq
12383

124-
/-- The natural map from `DeltaGeneratedSpace.of X` to `X`. -/
125-
def counit : (of X) → X := id
84+
@[deprecated (since := "2026-04-23")]
85+
alias DeltaGeneratedSpace.isOpen_iff := IsGeneratedBy.isOpen_iff
12686

127-
lemma continuous_counit : Continuous (counit : _ → X) := by
128-
rw [continuous_iff_coinduced_le]; exact deltaGenerated_le
87+
@[deprecated (since := "2026-04-23")]
88+
alias DeltaGeneratedSpace.continuous_iff := IsGeneratedBy.continuous_iff
12989

130-
/-- Delta-generated spaces are locally path-connected. -/
131-
instance [DeltaGeneratedSpace X] : LocPathConnectedSpace X := by
132-
rw [eq_deltaGenerated (X := X), deltaGenerated_eq_coinduced]
133-
exact LocPathConnectedSpace.coinduced _
90+
@[deprecated (since := "2026-04-23")]
91+
alias continuous_to_deltaGenerated := WithGeneratedByTopology.continuous_equiv
13492

135-
/-- Delta-generated spaces are sequential. -/
136-
instance [DeltaGeneratedSpace X] : SequentialSpace X := by
137-
rw [eq_deltaGenerated (X := X)]
138-
exact SequentialSpace.iSup fun p ↦ SequentialSpace.coinduced p.2
93+
@[deprecated (since := "2026-04-23")]
94+
alias deltaGeneratedSpace_deltaGenerated := IsGeneratedBy.instWithGeneratedByTopology
13995

140-
end DeltaGeneratedSpace
96+
@[deprecated (since := "2026-04-23")]
97+
alias deltaGenerated_mono := generatedBy_mono
98+
99+
@[deprecated (since := "2026-04-23")]
100+
alias DeltaGeneratedSpace.counit := WithGeneratedByTopology.equiv
101+
102+
@[deprecated (since := "2026-04-23")]
103+
alias DeltaGeneratedSpace.continuous_counit := WithGeneratedByTopology.continuous_equiv
104+
105+
@[deprecated (since := "2026-04-23")]
106+
alias DeltaGeneratedSpace.coinduced := IsGeneratedBy.coinduced
107+
108+
@[deprecated (since := "2026-04-23")]
109+
alias DeltaGeneratedSpace.iSup := IsGeneratedBy.iSup
110+
111+
@[deprecated (since := "2026-04-23")]
112+
alias DeltaGeneratedSpace.sup := IsGeneratedBy.sup
113+
114+
@[deprecated (since := "2026-04-23")]
115+
alias Topology.IsQuotientMap.deltaGeneratedSpace := Topology.IsQuotientMap.isGeneratedBy
116+
117+
@[deprecated (since := "2026-04-23")]
118+
alias Quot.deltaGeneratedSpace := Quot.isGeneratedBy
119+
120+
@[deprecated (since := "2026-04-23")]
121+
alias Quotient.deltaGeneratedSpace := Quotient.isGeneratedBy
122+
123+
@[deprecated (since := "2026-04-23")]
124+
alias Sum.deltaGeneratedSpace := Sum.isGeneratedBy
141125

142-
omit tY in
143-
/-- Any topology coinduced by a delta-generated topology is delta-generated. -/
144-
lemma DeltaGeneratedSpace.coinduced [DeltaGeneratedSpace X] (f : X → Y) :
145-
@DeltaGeneratedSpace Y (tX.coinduced f) :=
146-
let _ := tX.coinduced f
147-
⟨(continuous_to_deltaGenerated.2 continuous_coinduced_rng).coinduced_le⟩
148-
149-
/-- Suprema of delta-generated topologies are delta-generated. -/
150-
protected lemma DeltaGeneratedSpace.iSup {X : Type*} {ι : Sort*} {t : ι → TopologicalSpace X}
151-
(h : ∀ i, @DeltaGeneratedSpace X (t i)) : @DeltaGeneratedSpace X (⨆ i, t i) :=
152-
let _ := ⨆ i, t i
153-
⟨iSup_le_iff.2 fun i ↦ (h i).le_deltaGenerated.trans <| deltaGenerated_mono <| le_iSup t i⟩
154-
155-
/-- Suprema of delta-generated topologies are delta-generated. -/
156-
protected lemma DeltaGeneratedSpace.sup {X : Type*} {t₁ t₂ : TopologicalSpace X}
157-
(h₁ : @DeltaGeneratedSpace X t₁) (h₂ : @DeltaGeneratedSpace X t₂) :
158-
@DeltaGeneratedSpace X (t₁ ⊔ t₂) := by
159-
rw [sup_eq_iSup]
160-
exact .iSup <| Bool.forall_bool.2 ⟨h₂, h₁⟩
161-
162-
/-- Quotients of delta-generated spaces are delta-generated. -/
163-
lemma Topology.IsQuotientMap.deltaGeneratedSpace [DeltaGeneratedSpace X]
164-
{f : X → Y} (h : IsQuotientMap f) : DeltaGeneratedSpace Y :=
165-
h.isCoinducing.eq_coinduced ▸ DeltaGeneratedSpace.coinduced f
166-
167-
/-- Quotients of delta-generated spaces are delta-generated. -/
168-
instance Quot.deltaGeneratedSpace [DeltaGeneratedSpace X] {r : X → X → Prop} :
169-
DeltaGeneratedSpace (Quot r) :=
170-
isQuotientMap_quot_mk.deltaGeneratedSpace
171-
172-
/-- Quotients of delta-generated spaces are delta-generated. -/
173-
instance Quotient.deltaGeneratedSpace [DeltaGeneratedSpace X] {s : Setoid X} :
174-
DeltaGeneratedSpace (Quotient s) :=
175-
isQuotientMap_quotient_mk'.deltaGeneratedSpace
176-
177-
/-- Disjoint unions of delta-generated spaces are delta-generated. -/
178-
instance Sum.deltaGeneratedSpace [DeltaGeneratedSpace X] [DeltaGeneratedSpace Y] :
179-
DeltaGeneratedSpace (X ⊕ Y) :=
180-
DeltaGeneratedSpace.sup (.coinduced Sum.inl) (.coinduced Sum.inr)
181-
182-
/-- Disjoint unions of delta-generated spaces are delta-generated. -/
183-
instance Sigma.deltaGeneratedSpace {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
184-
[∀ i, DeltaGeneratedSpace (X i)] : DeltaGeneratedSpace (Σ i, X i) :=
185-
.iSup fun _ ↦ .coinduced _
126+
@[deprecated (since := "2026-04-23")]
127+
alias Sigma.deltaGeneratedSpace := Sigma.isGeneratedBy

0 commit comments

Comments
 (0)