From cfb341daebb67ad10f2ad2249cceacad21b266b5 Mon Sep 17 00:00:00 2001
From: Laurent Bartholdi <laurent.bartholdi@gmail.com>
Date: Sun, 3 Dec 2023 18:15:10 +0100
Subject: [PATCH] Added rubin

---
 Rubin.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Rubin.lean b/Rubin.lean
index de2e557..8f794dc 100644
--- a/Rubin.lean
+++ b/Rubin.lean
@@ -822,8 +822,12 @@ by
 
 end HomeoGroup
 
--- variables [topological_space α] [topological_space β] [continuous_mul_action G α] [continuous_mul_action G β]
--- noncomputable theorem rubin (hα : rubin_action G α) (hβ : rubin_action G β) : equivariant_homeomorph G α β := sorry
+variable [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α]
+         [TopologicalSpace β] [MulAction G β] [ContinuousMulAction G β]
+
+theorem rubin (hα : RubinAction G α) (hβ : RubinAction G β) : EquivariantHomeomorph G α β := by
+  sorry
+
 end Rubin
 
 end Rubin