🚚 Rename AssociatedPoset to RegularSupportBasis

Rubin.lean

@@ -707,108 +707,21 @@ section HomeoGroup
 
 open Topology
 
--- TODO: clean this lemma to not mention W anymore?
-lemma proposition_3_2_subset (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
-  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
-  [ContinuousMulAction G α]
-  {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) :
-  ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧
-  ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g ∧ RegularSupport α g ⊆ closure W :=
-by
-  have U_in_nhds : U ∈ 𝓝 p := by
-    rw [mem_nhds_iff]
-    use U
-
-  let ⟨W', W'_in_nhds, W'_ss_U, W'_compact⟩ := local_compact_nhds U_in_nhds
-
-  -- This feels like black magic, but okay
-  let ⟨W, _W_compact, W_closed, W'_ss_int_W, W_ss_U⟩ := exists_compact_closed_between W'_compact U_open W'_ss_U
-  have W_cl_eq_W : closure W = W := IsClosed.closure_eq W_closed
-
-  have W_in_nhds : W ∈ 𝓝 p := by
-    rw [mem_nhds_iff]
-    use interior W
-    repeat' apply And.intro
-    · exact interior_subset
-    · simp
-    · exact W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
-
-  use W
-
-  repeat' apply And.intro
-  exact W_in_nhds
-  {
-    rw [W_cl_eq_W]
-    exact W_ss_U
-  }
-
-  have p_in_int_W : p ∈ interior W := W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
-
-  let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G isOpen_interior p_in_int_W
-
-  use g
-  repeat' apply And.intro
-  · apply rigidStabilizer_mono interior_subset
-    simp
-    exact g_in_rist
-  · rw [<-mem_support] at g_moves_p
-    apply support_subset_regularSupport
-    exact g_moves_p
-  · rw [rigidStabilizer_support] at g_in_rist
-    apply subset_trans
-    exact regularSupport_subset_closure_support
-    apply closure_mono
-    apply subset_trans
-    exact g_in_rist
-    exact interior_subset
-
-theorem proposition_3_2 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
-  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
-  [hc : ContinuousMulAction G α] :
-  TopologicalSpace.IsTopologicalBasis (AssociatedPoset.asSet α) :=
-by
-  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-  {
-    intro U U_in_poset
-    rw [AssociatedPoset.mem_asSet] at U_in_poset
-    let ⟨T, T_val⟩ := U_in_poset
-    rw [<-T_val]
-    exact T.regular.isOpen
-  }
-  intro p U p_in_U U_open
-
-  let ⟨W, _, clW_ss_U, ⟨g, _, p_in_rsupp, rsupp_ss_clW⟩⟩ := proposition_3_2_subset G U_open p_in_U
-  use RegularSupport α g
-  repeat' apply And.intro
-  · rw [AssociatedPoset.mem_asSet']
-    constructor
-    exact ⟨p, p_in_rsupp⟩
-    use {(ContinuousMulAction.toHomeomorph α g : HomeoGroup α)}
-    unfold AssociatedPosetElem
-    simp
-    unfold RegularSupport
-    rw [<-homeoGroup_support_eq_support_toHomeomorph g]
-  · exact p_in_rsupp
-  · apply subset_trans
-    exact rsupp_ss_clW
-    exact clW_ss_U
-
--- TODO: implement Membership on AssociatedPoset
+-- TODO: implement Membership on RegularSupportBasis
 -- TODO: wrap these things in some neat structures
 theorem proposition_3_5 {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
   [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
   [hc : ContinuousMulAction G α]
-  (U : AssociatedPoset α) (F: Filter α):
-  (∃ p ∈ U.val, F.HasBasis (fun S: Set α => S ∈ AssociatedPoset.asSet α ∧ p ∈ S) id)
-  ↔ ∃ V : AssociatedPoset α, V ≤ U ∧ {W : AssociatedPoset α | W ≤ V} ⊆ { g •'' W | (g ∈ RigidStabilizer G U.val) (W ∈ F) }
+  (U : RegularSupportBasis α) (F: Filter α):
+  (∃ p ∈ U.val, F.HasBasis (fun S: Set α => S ∈ RegularSupportBasis.asSet α ∧ p ∈ S) id)
+  ↔ ∃ V : RegularSupportBasis α, V ≤ U ∧ {W : RegularSupportBasis α | W ≤ V} ⊆ { g •'' W | (g ∈ RigidStabilizer G U.val) (W ∈ F) (_: W ∈ RegularSupportBasis.asSet α) }
   :=
 by
   constructor
   {
     simp
     intro p p_in_U filter_basis
-    have assoc_poset_basis : TopologicalSpace.IsTopologicalBasis (AssociatedPoset.asSet α) := by
-      exact proposition_3_2 (G := G)
+    have assoc_poset_basis := RegularSupportBasis.isBasis G α
     have F_eq_nhds : F = 𝓝 p := by
       have nhds_basis := assoc_poset_basis.nhds_hasBasis (a := p)
       rw [<-filter_basis.filter_eq]

Rubin/HomeoGroup.lean

@@ -7,8 +7,7 @@ import Rubin.Topology
 import Rubin.Support
 import Rubin.RegularSupport
 
-structure HomeoGroup (α : Type _) [TopologicalSpace α] extends
-  Homeomorph α α
+structure HomeoGroup (α : Type _) [TopologicalSpace α] extends Homeomorph α α
 
 variable {α : Type _}
 variable [TopologicalSpace α]
@@ -156,7 +155,7 @@ theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) :
 
 namespace Rubin
 
-section AssociatedPoset.Prelude
+section RegularSupportBasis.Prelude
 
 variable {α : Type _}
 variable [TopologicalSpace α]
@@ -165,33 +164,39 @@ variable [DecidableEq α]
 /--
 Maps a "seed" of homeorphisms in α to the intersection of their regular support in α.
 
-Note that the condition that the resulting set is non-empty is introduced later in `AssociatedPosetSeed`
+Note that the condition that the resulting set is non-empty is introduced later in `RegularSupportBasis₀`
 --/
-def AssociatedPosetElem (S : Finset (HomeoGroup α)): Set α :=
-  ⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S)
+def RegularSupportInter₀ (S : Finset (HomeoGroup α)): Set α :=
+  ⋂ (g ∈ S), RegularSupport α g
+
+theorem RegularSupportInter₀.eq_sInter (S : Finset (HomeoGroup α)) :
+  RegularSupportInter₀ S = ⋂₀ ((fun (g : HomeoGroup α) => RegularSupport α g) '' S) :=
+by
+  rw [Set.sInter_image]
+  rfl
 
 /--
-This is a predecessor type to `AssociatedPoset`, where equality is defined on the `seed` used, rather than the `val`.
+This is a predecessor type to `RegularSupportBasis`, where equality is defined on the `seed` used, rather than the `val`.
 --/
-structure AssociatedPosetSeed (α : Type _) [TopologicalSpace α] where
+structure RegularSupportBasis₀ (α : Type _) [TopologicalSpace α] where
   seed : Finset (HomeoGroup α)
-  val_nonempty : Set.Nonempty (AssociatedPosetElem seed)
+  val_nonempty : Set.Nonempty (RegularSupportInter₀ seed)
 
-theorem AssociatedPosetSeed.eq_iff_seed_eq (S T : AssociatedPosetSeed α) : S = T ↔ S.seed = T.seed := by
+theorem RegularSupportBasis₀.eq_iff_seed_eq (S T : RegularSupportBasis₀ α) : S = T ↔ S.seed = T.seed := by
   -- Spooky :3c
   rw [mk.injEq]
 
-def AssociatedPosetSeed.val (S : AssociatedPosetSeed α) : Set α := AssociatedPosetElem S.seed
+def RegularSupportBasis₀.val (S : RegularSupportBasis₀ α) : Set α := RegularSupportInter₀ S.seed
 
-theorem AssociatedPosetSeed.val_def (S : AssociatedPosetSeed α) : S.val = AssociatedPosetElem S.seed := rfl
+theorem RegularSupportBasis₀.val_def (S : RegularSupportBasis₀ α) : S.val = RegularSupportInter₀ S.seed := rfl
 
 @[simp]
-theorem AssociatedPosetSeed.nonempty (S : AssociatedPosetSeed α) : Set.Nonempty S.val := S.val_nonempty
+theorem RegularSupportBasis₀.nonempty (S : RegularSupportBasis₀ α) : Set.Nonempty S.val := S.val_nonempty
 
 @[simp]
-theorem AssociatedPosetSeed.regular (S : AssociatedPosetSeed α) : Regular S.val := by
+theorem RegularSupportBasis₀.regular (S : RegularSupportBasis₀ α) : Regular S.val := by
   rw [S.val_def]
-  unfold AssociatedPosetElem
+  rw [RegularSupportInter₀.eq_sInter]
 
   apply regular_sInter
   · have set_decidable : DecidableEq (Set α) := Classical.typeDecidableEq (Set α)
@@ -205,10 +210,10 @@ theorem AssociatedPosetSeed.regular (S : AssociatedPosetSeed α) : Regular S.val
     rw [<-Heq]
     exact regularSupport_regular α g
 
-lemma AssociatedPosetElem.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α):
-  AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' AssociatedPosetElem seed :=
+lemma RegularSupportInter₀.mul_seed (seed : Finset (HomeoGroup α)) [DecidableEq (HomeoGroup α)] (f : HomeoGroup α):
+  RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) = f •'' RegularSupportInter₀ seed :=
 by
-  unfold AssociatedPosetElem
+  unfold RegularSupportInter₀
   simp
   conv => {
     rhs
@@ -220,110 +225,110 @@ by
 variable [DecidableEq (HomeoGroup α)]
 
 /--
-A `HomeoGroup α` group element `f` acts on an `AssociatedPosetSeed α` set `S`,
+A `HomeoGroup α` group element `f` acts on an `RegularSupportBasis₀ α` set `S`,
 by mapping each element `g` of `S.seed` to `f * g * f⁻¹`
 --/
-instance homeoGroup_smul₂ : SMul (HomeoGroup α) (AssociatedPosetSeed α) where
+instance homeoGroup_smul₂ : SMul (HomeoGroup α) (RegularSupportBasis₀ α) where
   smul := fun f S => ⟨
     (Finset.image (fun g => f * g * f⁻¹) S.seed),
     by
-      rw [AssociatedPosetElem.mul_seed]
+      rw [RegularSupportInter₀.mul_seed]
       simp
       exact S.val_nonempty
   ⟩
 
-theorem AssociatedPosetSeed.smul_seed (f : HomeoGroup α) (S : AssociatedPosetSeed α) :
+theorem RegularSupportBasis₀.smul_seed (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
   (f • S).seed = (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
 
-theorem AssociatedPosetSeed.smul_val (f : HomeoGroup α) (S : AssociatedPosetSeed α) :
-  (f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
+theorem RegularSupportBasis₀.smul_val (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
+  (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) := rfl
 
-theorem AssociatedPosetSeed.smul_val' (f : HomeoGroup α) (S : AssociatedPosetSeed α) :
+theorem RegularSupportBasis₀.smul_val' (f : HomeoGroup α) (S : RegularSupportBasis₀ α) :
   (f • S).val = f •'' S.val :=
 by
   unfold val
-  rw [<-AssociatedPosetElem.mul_seed]
-  rw [AssociatedPosetSeed.smul_seed]
+  rw [<-RegularSupportInter₀.mul_seed]
+  rw [RegularSupportBasis₀.smul_seed]
 
--- We define a "preliminary" group action from `HomeoGroup α` to `AssociatedPosetSeed`
-instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (AssociatedPosetSeed α) where
+-- We define a "preliminary" group action from `HomeoGroup α` to `RegularSupportBasis₀`
+instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (RegularSupportBasis₀ α) where
   one_smul := by
     intro S
-    rw [AssociatedPosetSeed.eq_iff_seed_eq]
-    rw [AssociatedPosetSeed.smul_seed]
+    rw [RegularSupportBasis₀.eq_iff_seed_eq]
+    rw [RegularSupportBasis₀.smul_seed]
     simp
   mul_smul := by
     intro f g S
-    rw [AssociatedPosetSeed.eq_iff_seed_eq]
-    repeat rw [AssociatedPosetSeed.smul_seed]
+    rw [RegularSupportBasis₀.eq_iff_seed_eq]
+    repeat rw [RegularSupportBasis₀.smul_seed]
     rw [Finset.image_image]
     ext x
     simp
     group
 
-end AssociatedPoset.Prelude
+end RegularSupportBasis.Prelude
 
 
 /--
 A partially-ordered set, associated to Rubin's proof.
 Any element in that set is made up of a `seed`,
-such that `val = AssociatedPosetElem seed` and `Set.Nonempty val`.
+such that `val = RegularSupportInter₀ seed` and `Set.Nonempty val`.
 
-Actions on this set are first defined in terms of `AssociatedPosetSeed`,
+Actions on this set are first defined in terms of `RegularSupportBasis₀`,
 as the proofs otherwise get hairy with a bunch of `Exists.choose` appearing.
 --/
-structure AssociatedPoset (α : Type _) [TopologicalSpace α] where
+structure RegularSupportBasis (α : Type _) [TopologicalSpace α] where
   val : Set α
-  val_has_seed : ∃ po_seed : AssociatedPosetSeed α, po_seed.val = val
+  val_has_seed : ∃ po_seed : RegularSupportBasis₀ α, po_seed.val = val
 
-namespace AssociatedPoset
+namespace RegularSupportBasis
 
 variable {α : Type _}
 variable [TopologicalSpace α]
 variable [DecidableEq α]
 
-theorem eq_iff_val_eq (S T : AssociatedPoset α) : S = T ↔ S.val = T.val := by
+theorem eq_iff_val_eq (S T : RegularSupportBasis α) : S = T ↔ S.val = T.val := by
   rw [mk.injEq]
 
-def fromSeed (seed : AssociatedPosetSeed α) : AssociatedPoset α := ⟨
+def fromSeed (seed : RegularSupportBasis₀ α) : RegularSupportBasis α := ⟨
   seed.val,
   ⟨seed, seed.val_def⟩
 ⟩
 
-noncomputable def full_seed (S : AssociatedPoset α) : AssociatedPosetSeed α :=
+noncomputable def full_seed (S : RegularSupportBasis α) : RegularSupportBasis₀ α :=
   (Exists.choose S.val_has_seed)
 
-noncomputable def seed (S : AssociatedPoset α) : Finset (HomeoGroup α) :=
+noncomputable def seed (S : RegularSupportBasis α) : Finset (HomeoGroup α) :=
   S.full_seed.seed
 
 @[simp]
-theorem full_seed_seed (S : AssociatedPoset α) : S.full_seed.seed = S.seed := rfl
+theorem full_seed_seed (S : RegularSupportBasis α) : S.full_seed.seed = S.seed := rfl
 
 @[simp]
-theorem fromSeed_val (seed : AssociatedPosetSeed α) :
+theorem fromSeed_val (seed : RegularSupportBasis₀ α) :
   (fromSeed seed).val = seed.val :=
 by
   unfold fromSeed
   simp
 
 @[simp]
-theorem val_from_seed (S : AssociatedPoset α) : AssociatedPosetElem S.seed = S.val := by
+theorem val_from_seed (S : RegularSupportBasis α) : RegularSupportInter₀ S.seed = S.val := by
   unfold seed full_seed
-  rw [<-AssociatedPosetSeed.val_def]
+  rw [<-RegularSupportBasis₀.val_def]
   rw [Exists.choose_spec S.val_has_seed]
 
 @[simp]
-theorem val_from_seed₂ (S : AssociatedPoset α) : S.full_seed.val = S.val := by
+theorem val_from_seed₂ (S : RegularSupportBasis α) : S.full_seed.val = S.val := by
   unfold full_seed
-  rw [AssociatedPosetSeed.val_def]
+  rw [RegularSupportBasis₀.val_def]
   nth_rw 2 [<-val_from_seed]
   unfold seed full_seed
   rfl
 
--- Allows one to prove properties of AssociatedPoset without jumping through `Exists.choose`-shaped hoops
+-- Allows one to prove properties of RegularSupportBasis without jumping through `Exists.choose`-shaped hoops
 theorem prop_from_val {p : Set α → Prop}
-  (any_seed : ∀ po_seed : AssociatedPosetSeed α, p po_seed.val) :
-  ∀ (S : AssociatedPoset α), p S.val :=
+  (any_seed : ∀ po_seed : RegularSupportBasis₀ α, p po_seed.val) :
+  ∀ (S : RegularSupportBasis α), p S.val :=
 by
   intro S
   rw [<-val_from_seed]
@@ -333,45 +338,45 @@ by
   exact res
 
 @[simp]
-theorem nonempty : ∀ (S : AssociatedPoset α), Set.Nonempty S.val :=
-  prop_from_val AssociatedPosetSeed.nonempty
+theorem nonempty : ∀ (S : RegularSupportBasis α), Set.Nonempty S.val :=
+  prop_from_val RegularSupportBasis₀.nonempty
 
 @[simp]
-theorem regular : ∀ (S : AssociatedPoset α), Regular S.val :=
-  prop_from_val AssociatedPosetSeed.regular
+theorem regular : ∀ (S : RegularSupportBasis α), Regular S.val :=
+  prop_from_val RegularSupportBasis₀.regular
 
 variable [DecidableEq (HomeoGroup α)]
 
-instance homeoGroup_smul₃ : SMul (HomeoGroup α) (AssociatedPoset α) where
+instance homeoGroup_smul₃ : SMul (HomeoGroup α) (RegularSupportBasis α) where
   smul := fun f S => ⟨
     f •'' S.val,
     by
       use f • S.full_seed
-      rw [AssociatedPosetSeed.smul_val']
+      rw [RegularSupportBasis₀.smul_val']
       simp
   ⟩
 
-theorem smul_val (f : HomeoGroup α) (S : AssociatedPoset α) :
+theorem smul_val (f : HomeoGroup α) (S : RegularSupportBasis α) :
   (f • S).val = f •'' S.val := rfl
 
-theorem smul_seed' (f : HomeoGroup α) (S : AssociatedPoset α) (seed : Finset (HomeoGroup α)) :
-  S.val = AssociatedPosetElem seed →
-  (f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) seed) :=
+theorem smul_seed' (f : HomeoGroup α) (S : RegularSupportBasis α) (seed : Finset (HomeoGroup α)) :
+  S.val = RegularSupportInter₀ seed →
+  (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) seed) :=
 by
   intro S_val_eq
   rw [smul_val]
-  rw [AssociatedPosetElem.mul_seed]
+  rw [RegularSupportInter₀.mul_seed]
   rw [S_val_eq]
 
-theorem smul_seed (f : HomeoGroup α) (S : AssociatedPoset α) :
-  (f • S).val = AssociatedPosetElem (Finset.image (fun g => f * g * f⁻¹) S.seed) :=
+theorem smul_seed (f : HomeoGroup α) (S : RegularSupportBasis α) :
+  (f • S).val = RegularSupportInter₀ (Finset.image (fun g => f * g * f⁻¹) S.seed) :=
 by
   apply smul_seed'
   symm
   exact val_from_seed S
 
 -- Note: we could potentially implement MulActionHom
-instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (AssociatedPoset α) where
+instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (RegularSupportBasis α) where
   one_smul := by
     intro S
     rw [eq_iff_val_eq]
@@ -383,14 +388,14 @@ instance homeoGroup_mulAction₃ : MulAction (HomeoGroup α) (AssociatedPoset α
     repeat rw [smul_val]
     rw [smulImage_mul]
 
-instance associatedPoset_le : LE (AssociatedPoset α) where
+instance associatedPoset_le : LE (RegularSupportBasis α) where
   le := fun S T => S.val ⊆ T.val
 
-theorem le_def (S T : AssociatedPoset α) : S ≤ T ↔ S.val ⊆ T.val := by
+theorem le_def (S T : RegularSupportBasis α) : S ≤ T ↔ S.val ⊆ T.val := by
   rw [iff_eq_eq]
   rfl
 
-instance associatedPoset_partialOrder : PartialOrder (AssociatedPoset α) where
+instance associatedPoset_partialOrder : PartialOrder (RegularSupportBasis α) where
   le_refl := fun S => (le_def S S).mpr (le_refl S.val)
   le_trans := fun S T U S_le_T S_le_U => (le_def S U).mpr (le_trans
     ((le_def _ _).mp S_le_T)
@@ -403,7 +408,7 @@ instance associatedPoset_partialOrder : PartialOrder (AssociatedPoset α) where
     rw [eq_iff_val_eq]
     apply le_antisymm <;> assumption
 
-theorem smul_mono {S T : AssociatedPoset α} (f : HomeoGroup α) (S_le_T : S ≤ T) :
+theorem smul_mono {S T : RegularSupportBasis α} (f : HomeoGroup α) (S_le_T : S ≤ T) :
   f • S ≤ f • T :=
 by
   rw [le_def]
@@ -411,23 +416,23 @@ by
   apply smulImage_mono
   assumption
 
-instance associatedPoset_coeSet : Coe (AssociatedPoset α) (Set α) where
-  coe := AssociatedPoset.val
+instance associatedPoset_coeSet : Coe (RegularSupportBasis α) (Set α) where
+  coe := RegularSupportBasis.val
 
 def asSet (α : Type _) [TopologicalSpace α]: Set (Set α) :=
-  { S : Set α | ∃ T : AssociatedPoset α, T.val = S }
+  { S : Set α | ∃ T : RegularSupportBasis α, T.val = S }
 
 theorem asSet_def :
-  AssociatedPoset.asSet α = { S : Set α | ∃ T : AssociatedPoset α, T.val = S } := rfl
+  RegularSupportBasis.asSet α = { S : Set α | ∃ T : RegularSupportBasis α, T.val = S } := rfl
 
 theorem mem_asSet (S : Set α) :
-  S ∈ AssociatedPoset.asSet α ↔ ∃ T : AssociatedPoset α, T.val = S :=
+  S ∈ RegularSupportBasis.asSet α ↔ ∃ T : RegularSupportBasis α, T.val = S :=
 by
   rw [asSet_def]
   simp
 
 theorem mem_asSet' (S : Set α) :
-  S ∈ AssociatedPoset.asSet α ↔ Set.Nonempty S ∧ ∃ seed : Finset (HomeoGroup α), S = AssociatedPosetElem seed :=
+  S ∈ RegularSupportBasis.asSet α ↔ Set.Nonempty S ∧ ∃ seed : Finset (HomeoGroup α), S = RegularSupportInter₀ seed :=
 by
   rw [asSet_def]
   simp
@@ -438,7 +443,7 @@ by
     simp
 
     let ⟨⟨seed, _⟩, eq⟩ := T.val_has_seed
-    rw [AssociatedPosetSeed.val_def] at eq
+    rw [RegularSupportBasis₀.val_def] at eq
     simp at eq
     use seed
     exact eq.symm
@@ -447,12 +452,113 @@ by
     use fromSeed ⟨seed, S_nonempty⟩
     rw [val_from_seed]
     simp
-    rw [AssociatedPosetSeed.val_def]
+    rw [RegularSupportBasis₀.val_def]
+
+instance membership : Membership α (RegularSupportBasis α) where
+  mem := fun x S => x ∈ S.val
+
+theorem mem_iff (x : α) (S : RegularSupportBasis α) : x ∈ S ↔ x ∈ (S : Set α) := iff_eq_eq ▸ rfl
+
+section Basis
+open Topology
+
+-- TODO: clean this lemma to not mention W anymore?
+lemma proposition_3_2_subset (G : Type _) {α : Type _} [Group G] [TopologicalSpace α] [MulAction G α]
+  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
+  [ContinuousMulAction G α]
+  {U : Set α} (U_open : IsOpen U) {p : α} (p_in_U : p ∈ U) :
+  ∃ (W : Set α), W ∈ 𝓝 p ∧ closure W ⊆ U ∧
+  ∃ (g : G), g ∈ RigidStabilizer G W ∧ p ∈ RegularSupport α g ∧ RegularSupport α g ⊆ closure W :=
+by
+  have U_in_nhds : U ∈ 𝓝 p := by
+    rw [mem_nhds_iff]
+    use U
+
+  let ⟨W', W'_in_nhds, W'_ss_U, W'_compact⟩ := local_compact_nhds U_in_nhds
+
+  -- This feels like black magic, but okay
+  let ⟨W, _W_compact, W_closed, W'_ss_int_W, W_ss_U⟩ := exists_compact_closed_between W'_compact U_open W'_ss_U
+  have W_cl_eq_W : closure W = W := IsClosed.closure_eq W_closed
+
+  have W_in_nhds : W ∈ 𝓝 p := by
+    rw [mem_nhds_iff]
+    use interior W
+    repeat' apply And.intro
+    · exact interior_subset
+    · simp
+    · exact W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
+
+  use W
+
+  repeat' apply And.intro
+  exact W_in_nhds
+  {
+    rw [W_cl_eq_W]
+    exact W_ss_U
+  }
 
-end AssociatedPoset
+  have p_in_int_W : p ∈ interior W := W'_ss_int_W (mem_of_mem_nhds W'_in_nhds)
+
+  let ⟨g, g_in_rist, g_moves_p⟩ := get_moving_elem_in_rigidStabilizer G isOpen_interior p_in_int_W
+
+  use g
+  repeat' apply And.intro
+  · apply rigidStabilizer_mono interior_subset
+    simp
+    exact g_in_rist
+  · rw [<-mem_support] at g_moves_p
+    apply support_subset_regularSupport
+    exact g_moves_p
+  · rw [rigidStabilizer_support] at g_in_rist
+    apply subset_trans
+    exact regularSupport_subset_closure_support
+    apply closure_mono
+    apply subset_trans
+    exact g_in_rist
+    exact interior_subset
+
+/--
+## Proposition 3.2 : RegularSupportBasis is a topological basis of `α`
+-/
+theorem isBasis (G α : Type _) [Group G] [TopologicalSpace α] [MulAction G α]
+  [T2Space α] [LocallyCompactSpace α] [h_ld : LocallyDense G α] [HasNoIsolatedPoints α]
+  [hc : ContinuousMulAction G α] :
+  TopologicalSpace.IsTopologicalBasis (RegularSupportBasis.asSet α) :=
+by
+  apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
+  {
+    intro U U_in_poset
+    rw [RegularSupportBasis.mem_asSet] at U_in_poset
+    let ⟨T, T_val⟩ := U_in_poset
+    rw [<-T_val]
+    exact T.regular.isOpen
+  }
+  intro p U p_in_U U_open
+
+  let ⟨W, _, clW_ss_U, ⟨g, _, p_in_rsupp, rsupp_ss_clW⟩⟩ := proposition_3_2_subset G U_open p_in_U
+  use RegularSupport α g
+  repeat' apply And.intro
+  · rw [RegularSupportBasis.mem_asSet']
+    constructor
+    exact ⟨p, p_in_rsupp⟩
+    use {(ContinuousMulAction.toHomeomorph α g : HomeoGroup α)}
+    unfold RegularSupportInter₀
+    simp
+    unfold RegularSupport
+    rw [<-homeoGroup_support_eq_support_toHomeomorph g]
+  · exact p_in_rsupp
+  · apply subset_trans
+    exact rsupp_ss_clW
+    exact clW_ss_U
+
+end Basis
+end RegularSupportBasis
 
 section Other
 
+/--
+## Proposition 3.1
+--/
 theorem homeoGroup_rigidStabilizer_subset_iff {α : Type _} [TopologicalSpace α]
   [h_lm : LocallyMoving (HomeoGroup α) α]
   {U V : Set α} (U_reg : Regular U) (V_reg : Regular V):