From 23d08212903d502825e288b287f92d29d2c842d2 Mon Sep 17 00:00:00 2001 From: Adrien Burgun Date: Sun, 17 Dec 2023 01:08:28 +0100 Subject: [PATCH] :sparkles: Almost complete proof of proposition 3.5 --- Rubin.lean | 273 +++++++++++++++++++++++++++------ Rubin/HomeoGroup.lean | 93 ++++++++++- Rubin/InteriorClosure.lean | 7 + Rubin/RegularSupportBasis.lean | 72 +++++++-- 4 files changed, 383 insertions(+), 62 deletions(-) diff --git a/Rubin.lean b/Rubin.lean index 37b6d98..973b273 100644 --- a/Rubin.lean +++ b/Rubin.lean @@ -47,13 +47,9 @@ theorem equiv_congr_ne {ι ι' : Type _} (e : ι ≃ ι') {x y : ι} : x ≠ y ---------------------------------------------------------------- section Rubin -variable {G α β : Type _} [Group G] - ---------------------------------------------------------------- section RubinActions -variable [TopologicalSpace α] [TopologicalSpace β] - structure RubinAction (G α : Type _) extends Group G, TopologicalSpace α, @@ -699,16 +695,18 @@ by repeat rw [<-proposition_2_1] exact alg_disj +#check proposition_2_1 lemma rigidStabilizerInter_eq_algebraicCentralizerInter {S : Finset G} : RigidStabilizerInter₀ α S = AlgebraicCentralizerInter₀ S := by unfold RigidStabilizerInter₀ unfold AlgebraicCentralizerInter₀ - conv => { - lhs - congr; intro; congr; intro - rw [<-proposition_2_1] - } + simp only [<-proposition_2_1] + -- conv => { + -- rhs + -- congr; intro; congr; intro + -- rw [proposition_2_1 (α := α)] + -- } theorem rigidStabilizerBasis_eq_algebraicCentralizerBasis : AlgebraicCentralizerBasis G = RigidStabilizerBasis G α := @@ -744,44 +742,231 @@ open Topology variable {G α : Type _} [Group G] [TopologicalSpace α] [T2Space α] variable [MulAction G α] [ContinuousMulAction G α] [FaithfulSMul G α] [LocallyMoving G α] -#check RegularSupportBasis.asSet -#check RigidStabilizerBasis - --- TODO: implement Smul of G on RigidStabilizerBasis? - --- theorem regularSupportBasis_eq_ridigStabilizerBasis : --- RegularSupportBasis.asSet α = RigidStabilizerBasis (HomeoGroup α) α := --- by --- sorry - --- 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 : 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 := 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] --- rw [<-nhds_basis.filter_eq] --- have p_in_int_cl := h_ld.isLocallyDense U U.regular.isOpen p p_in_U --- -- TODO: show that ∃ V ⊆ closure (orbit (rist G U) p) - --- sorry --- } --- sorry +example : TopologicalSpace G := TopologicalSpace.generateFrom (RigidStabilizerBasis.asSets G α) + +-- TODO: remove +-- proposition_3_4_1 +example {α : Type _} [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] (F : Ultrafilter α) (p : α): + F ≤ 𝓝 p ↔ p ∈ ⋂ (S ∈ F), closure S := +by + rw [<-Ultrafilter.clusterPt_iff] + simp + exact clusterPt_iff_forall_mem_closure + +theorem proposition_3_4_2 {α : Type _} [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] (F : Ultrafilter α): + (∃ p : α, ClusterPt p F) ↔ ∃ S ∈ F, IsCompact (closure S) := +by + constructor + · intro ⟨p, p_clusterPt⟩ + rw [Ultrafilter.clusterPt_iff] at p_clusterPt + have ⟨S, S_in_nhds, S_compact⟩ := (compact_basis_nhds p).ex_mem + use S + constructor + exact p_clusterPt S_in_nhds + rw [IsClosed.closure_eq S_compact.isClosed] + exact S_compact + · intro ⟨S, S_in_F, clS_compact⟩ + have F_le_principal_S : F ≤ Filter.principal (closure S) := by + rw [Filter.le_principal_iff] + simp + apply Filter.sets_of_superset + exact S_in_F + exact subset_closure + let ⟨x, _, F_clusterPt⟩ := clS_compact F_le_principal_S + use x + +def RSuppSubsets {α : Type _} [TopologicalSpace α] (V : Set α) : Set (Set α) := + {W ∈ RegularSupportBasis.asSet α | W ⊆ V} + +def RSuppOrbit {G α : Type _} [Group G] [TopologicalSpace α] [MulAction G α] (F : Filter α) (H : Subgroup G) : Set (Set α) := + { g •'' W | (g ∈ H) (W ∈ F) } + +lemma moving_elem_of_open_subset_closure_orbit {U V : Set α} (U_open : IsOpen U) {p : α} + (U_ss_clOrbit : U ⊆ closure (MulAction.orbit (RigidStabilizer G V) p)) : + ∃ h : G, h ∈ RigidStabilizer G V ∧ h • p ∈ U := +by + -- Idea: can `Support α g ⊆ MulAction.orbit (RigidStabilizer G (RegularSupport α g)) p` be proven? + sorry + +lemma compact_subset_of_rsupp_basis [LocallyCompactSpace α] + (U : RegularSupportBasis α): + ∃ V : RegularSupportBasis α, (closure V.val) ⊆ U.val ∧ IsCompact (closure V.val) := +by + -- Idea: use (RegularSupportBasis.isBasis G α).nhds_hasBasis and compact_basis_nhds together? + -- Note: exists_compact_subset is *very* close to this theorem + sorry + +theorem proposition_3_5 [LocallyDense G α] [LocallyCompactSpace α] [HasNoIsolatedPoints α] + (U : RegularSupportBasis α) (F: Ultrafilter α): + (∃ p ∈ U.val, ClusterPt p F) + ↔ ∃ V : RegularSupportBasis α, V ≤ U ∧ RSuppSubsets V.val ⊆ RSuppOrbit F (RigidStabilizer G U.val) := +by + constructor + { + simp + intro p p_in_U p_clusterPt + have U_open : IsOpen U.val := U.regular.isOpen + + -- First, get a neighborhood of p that is a subset of the closure of the orbit of G_U + have clOrbit_in_nhds := LocallyDense.rigidStabilizer_in_nhds G α U_open p_in_U + rw [mem_nhds_iff] at clOrbit_in_nhds + let ⟨V, V_ss_clOrbit, V_open, p_in_V⟩ := clOrbit_in_nhds + clear clOrbit_in_nhds + + -- Then, get a nontrivial element from that set + let ⟨g, g_in_rist, g_ne_one⟩ := LocallyMoving.get_nontrivial_rist_elem (G := G) V_open ⟨p, p_in_V⟩ + + -- Somehow, the regular support of g is within U + have rsupp_ss_U : RegularSupport α g ⊆ U.val := by + rw [RegularSupport, InteriorClosure] + + apply interiorClosure_subset_of_regular _ U.regular + rw [<-rigidStabilizer_support] + apply rigidStabilizer_mono _ g_in_rist + + show V ⊆ U.val + -- Would probably require showing that the orbit of the rigidstabilizer is a subset of U + sorry + + -- Use as the chosen set RegularSupport g + let g' : HomeoGroup α := HomeoGroup.fromContinuous α g + have g'_ne_one : g' ≠ 1 := by + simp + rw [<-HomeoGroup.fromContinuous_one (G := G)] + rw [HomeoGroup.fromContinuous_eq_iff] + exact g_ne_one + use RegularSupportBasis.fromSingleton g' g'_ne_one + + constructor + · -- This statement is equivalent to rsupp(g) ⊆ U + rw [RegularSupportBasis.le_def] + rw [RegularSupportBasis.fromSingleton_val] + unfold RegularSupportInter₀ + simp + exact rsupp_ss_U + · intro W W_in_subsets + rw [RegularSupportBasis.fromSingleton_val] at W_in_subsets + unfold RSuppSubsets RegularSupportInter₀ at W_in_subsets + simp at W_in_subsets + let ⟨W_in_basis, W_subset_rsupp⟩ := W_in_subsets + clear W_in_subsets g' g'_ne_one + + -- We have that W is a subset of the closure of the orbit of G_U + have W_ss_clOrbit : W ⊆ closure (MulAction.orbit (↥(RigidStabilizer G U.val)) p) := by + rw [rigidStabilizer_support] at g_in_rist + calc + W ⊆ RegularSupport α g := by assumption + _ ⊆ closure (Support α g) := regularSupport_subset_closure_support + _ ⊆ closure V := by + apply closure_mono + assumption + _ ⊆ _ := by + rw [<-closure_closure (s := MulAction.orbit _ _)] + apply closure_mono + assumption + unfold RSuppOrbit + simp + + have W_open : IsOpen W := by + let ⟨W', W'_eq⟩ := (RegularSupportBasis.mem_asSet _).mp W_in_basis + rw [<-W'_eq] + exact W'.regular.isOpen + have W_nonempty : Set.Nonempty W := by + let ⟨W', W'_eq⟩ := (RegularSupportBasis.mem_asSet _).mp W_in_basis + rw [<-W'_eq] + exact W'.nonempty + + -- We get an element `h` such that `h • p ∈ W` and `h ∈ G_U` + let ⟨h, h_in_rist, hp_in_W⟩ := moving_elem_of_open_subset_closure_orbit W_open W_ss_clOrbit + + use h + constructor + exact h_in_rist + + use h⁻¹ •'' W + constructor + swap + { + rw [smulImage_mul] + simp + } + + -- We just need to show that h⁻¹ •'' W ∈ F, that is, h⁻¹ •'' W ∈ 𝓝 p + rw [Ultrafilter.clusterPt_iff] at p_clusterPt + apply p_clusterPt + + have basis := (RegularSupportBasis.isBasis G α).nhds_hasBasis (a := p) + rw [basis.mem_iff] + use h⁻¹ •'' W + repeat' apply And.intro + · rw [RegularSupportBasis.mem_asSet] + rw [RegularSupportBasis.mem_asSet] at W_in_basis + let ⟨W', W'_eq⟩ := W_in_basis + have dec_eq : DecidableEq (HomeoGroup α) := Classical.decEq _ + use (HomeoGroup.fromContinuous α h⁻¹) • W' + rw [RegularSupportBasis.smul_val, W'_eq] + simp + · rw [mem_smulImage, inv_inv] + exact hp_in_W + · exact Eq.subset rfl + } + { + intro ⟨V, ⟨V_ss_U, subsets_ss_orbit⟩⟩ + rw [RegularSupportBasis.le_def] at V_ss_U + + -- Obtain a compact subset of V' in the basis + let ⟨V', clV'_ss_V, clV'_compact⟩ := compact_subset_of_rsupp_basis V + + have V'_in_subsets : V'.val ∈ RSuppSubsets V.val := by + unfold RSuppSubsets + simp + constructor + unfold RegularSupportBasis.asSet + simp + exact subset_trans subset_closure clV'_ss_V + + -- V' is in the orbit, so there exists a value `g ∈ G_U` such that `gV ∈ F` + -- Note that with the way we set up the equations, we obtain `g⁻¹` + have V'_in_orbit := subsets_ss_orbit V'_in_subsets + simp [RSuppOrbit] at V'_in_orbit + let ⟨g, g_in_rist, ⟨W, W_in_F, gW_eq_V⟩⟩ := V'_in_orbit + + have gV'_in_F : g⁻¹ •'' V' ∈ F := by + rw [smulImage_inv] at gW_eq_V + rw [<-gW_eq_V] + assumption + have gV'_compact : IsCompact (closure (g⁻¹ •'' V'.val)) := by + rw [smulImage_closure _ _ (continuousMulAction_elem_continuous α g⁻¹)] + -- TODO: smulImage_compact + sorry + + have ⟨p, p_lim⟩ := (proposition_3_4_2 F).mpr ⟨g⁻¹ •'' V'.val, ⟨gV'_in_F, gV'_compact⟩⟩ + use p + constructor + swap + assumption + + rw [clusterPt_iff_forall_mem_closure] at p_lim + specialize p_lim (g⁻¹ •'' V') gV'_in_F + rw [smulImage_closure _ _ (continuousMulAction_elem_continuous α g⁻¹)] at p_lim + rw [mem_smulImage, inv_inv] at p_lim + + rw [rigidStabilizer_support] at g_in_rist + rw [<-support_inv] at g_in_rist + have q := fixed_smulImage_in_support g⁻¹ g_in_rist + rw [<-fixed_smulImage_in_support g⁻¹ g_in_rist] + + rw [mem_smulImage, inv_inv] + apply V_ss_U + apply clV'_ss_V + exact p_lim + } end HomeoGroup +variable {G α β : Type _} +variable [Group G] + variable [TopologicalSpace α] [MulAction G α] [ContinuousMulAction G α] [TopologicalSpace β] [MulAction G β] [ContinuousMulAction G β] diff --git a/Rubin/HomeoGroup.lean b/Rubin/HomeoGroup.lean index 2f70ca7..ceaedb3 100644 --- a/Rubin/HomeoGroup.lean +++ b/Rubin/HomeoGroup.lean @@ -140,18 +140,99 @@ instance homeoGroup_mulAction₁_faithful : FaithfulSMul (HomeoGroup α) α wher simp exact hyp x -theorem homeoGroup_support_eq_support_toHomeomorph {G : Type _} - [Group G] [MulAction G α] [Rubin.ContinuousMulAction G α] (g : G) : - Rubin.Support α g = Rubin.Support α (HomeoGroup.from (Rubin.ContinuousMulAction.toHomeomorph α g)) := +theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) : + g •'' S = ⇑g.toHomeomorph '' S := rfl + +section ContinuousMulActionCoe + +variable {G : Type _} [Group G] +variable [MulAction G α] [Rubin.ContinuousMulAction G α] + +/-- +`fromContinuous` is a structure-preserving transformation from a continuous `MulAction` to a `HomeoGroup` +--/ +def HomeoGroup.fromContinuous (α : Type _) [TopologicalSpace α] [MulAction G α] [Rubin.ContinuousMulAction G α] + (g : G) : HomeoGroup α := + HomeoGroup.from (Rubin.ContinuousMulAction.toHomeomorph α g) + +@[simp] +theorem HomeoGroup.fromContinuous_def (g : G) : + HomeoGroup.from (Rubin.ContinuousMulAction.toHomeomorph α g) = HomeoGroup.fromContinuous α g := rfl + +-- instance homeoGroup_coe_fromContinuous : Coe G (HomeoGroup α) where +-- coe := fun g => HomeoGroup.fromContinuous α g + +@[simp] +theorem HomeoGroup.fromContinuous_smul (g : G) : + ∀ x : α, (HomeoGroup.fromContinuous α g) • x = g • x := +by + intro x + unfold fromContinuous + rw [<-HomeoGroup.smul₁_def', HomeoGroup.from_toHomeomorph] + unfold Rubin.ContinuousMulAction.toHomeomorph + simp + +theorem HomeoGroup.fromContinuous_one : + HomeoGroup.fromContinuous α (1 : G) = (1 : HomeoGroup α) := +by + apply FaithfulSMul.eq_of_smul_eq_smul (α := α) + simp + +theorem HomeoGroup.fromContinuous_mul (g h : G): + (HomeoGroup.fromContinuous α g) * (HomeoGroup.fromContinuous α h) = (HomeoGroup.fromContinuous α (g * h)) := +by + apply FaithfulSMul.eq_of_smul_eq_smul (α := α) + intro x + rw [mul_smul] + simp + rw [mul_smul] + +theorem HomeoGroup.fromContinuous_inv (g : G): + HomeoGroup.fromContinuous α g⁻¹ = (HomeoGroup.fromContinuous α g)⁻¹ := +by + apply FaithfulSMul.eq_of_smul_eq_smul (α := α) + intro x + group_action + rw [mul_smul] + simp + +theorem HomeoGroup.fromContinuous_eq_iff [FaithfulSMul G α] (g h : G): + (HomeoGroup.fromContinuous α g) = (HomeoGroup.fromContinuous α h) ↔ g = h := +by + constructor + · intro cont_eq + apply FaithfulSMul.eq_of_smul_eq_smul (α := α) + intro x + rw [<-HomeoGroup.fromContinuous_smul g] + rw [cont_eq] + simp + · tauto + +@[simp] +theorem HomeoGroup.fromContinuous_support (g : G) : + Rubin.Support α (HomeoGroup.fromContinuous α g) = Rubin.Support α g := by ext x repeat rw [Rubin.mem_support] - rw [<-HomeoGroup.smul₁_def] + rw [<-HomeoGroup.smul₁_def, <-HomeoGroup.fromContinuous_def] rw [HomeoGroup.from_toHomeomorph] rw [Rubin.ContinuousMulAction.toHomeomorph_toFun] -theorem HomeoGroup.smulImage_eq_image (g : HomeoGroup α) (S : Set α) : - g •'' S = ⇑g.toHomeomorph '' S := rfl +@[simp] +theorem HomeoGroup.fromContinuous_regularSupport (g : G) : + Rubin.RegularSupport α (HomeoGroup.fromContinuous α g) = Rubin.RegularSupport α g := +by + unfold Rubin.RegularSupport + rw [HomeoGroup.fromContinuous_support] + +@[simp] +theorem HomeoGroup.fromContinuous_smulImage (g : G) (V : Set α) : + (HomeoGroup.fromContinuous α g) •'' V = g •'' V := +by + repeat rw [Rubin.smulImage_def] + simp + +end ContinuousMulActionCoe namespace Rubin diff --git a/Rubin/InteriorClosure.lean b/Rubin/InteriorClosure.lean index a2a6b14..dc2382e 100644 --- a/Rubin/InteriorClosure.lean +++ b/Rubin/InteriorClosure.lean @@ -97,6 +97,13 @@ theorem monotone_interiorClosure : Monotone (InteriorClosure (α := α)) := fun a b => interiorClosure_mono a b +theorem interiorClosure_subset_of_regular {U V : Set α} (U_ss_V : U ⊆ V) (V_regular : Regular V) : + InteriorClosure U ⊆ V := +by + rw [<-V_regular] + apply interiorClosure_mono + assumption + theorem compl_closure_regular_of_open {S : Set α} (S_open : IsOpen S) : Regular (closure S)ᶜ := by apply Set.eq_of_subset_of_subset · simp diff --git a/Rubin/RegularSupportBasis.lean b/Rubin/RegularSupportBasis.lean index 8b4b271..7c01623 100644 --- a/Rubin/RegularSupportBasis.lean +++ b/Rubin/RegularSupportBasis.lean @@ -126,7 +126,7 @@ instance homeoGroup_mulAction₂ : MulAction (HomeoGroup α) (RegularSupportBasi end RegularSupportBasis.Prelude - +-- TODO: define RegularSupportBasis as a Set directly? /-- A partially-ordered set, associated to Rubin's proof. Any element in that set is made up of a `seed`, @@ -153,18 +153,44 @@ def fromSeed (seed : RegularSupportBasis₀ α) : RegularSupportBasis α := ⟨ ⟨seed, seed.val_def⟩ ⟩ +def fromSingleton [T2Space α] (g : HomeoGroup α) (g_ne_one : g ≠ 1) : RegularSupportBasis α := + let seed : RegularSupportBasis₀ α := ⟨ + {g}, + by + unfold RegularSupportInter₀ + simp + rw [Set.nonempty_iff_ne_empty] + intro rsupp_empty + apply g_ne_one + apply FaithfulSMul.eq_of_smul_eq_smul (α := α) + intro x + simp + rw [<-not_mem_support] + apply Set.not_mem_subset + · apply support_subset_regularSupport + · rw [rsupp_empty] + exact Set.not_mem_empty x + ⟩ + fromSeed seed + +theorem fromSingleton_val [T2Space α] (g : HomeoGroup α) (g_ne_one : g ≠ 1) : + (fromSingleton g g_ne_one).val = RegularSupportInter₀ {g} := rfl + noncomputable def full_seed (S : RegularSupportBasis α) : RegularSupportBasis₀ α := (Exists.choose S.val_has_seed) noncomputable def seed (S : RegularSupportBasis α) : Finset (HomeoGroup α) := S.full_seed.seed +instance : Coe (RegularSupportBasis₀ α) (RegularSupportBasis α) where + coe := fromSeed + @[simp] theorem full_seed_seed (S : RegularSupportBasis α) : S.full_seed.seed = S.seed := rfl @[simp] theorem fromSeed_val (seed : RegularSupportBasis₀ α) : - (fromSeed seed).val = seed.val := + (seed : RegularSupportBasis α).val = seed.val := by unfold fromSeed simp @@ -320,10 +346,13 @@ theorem mem_iff (x : α) (S : RegularSupportBasis α) : x ∈ S ↔ x ∈ (S : S section Basis open Topology +variable (G α : Type _) +variable [Group G] +variable [TopologicalSpace α] [T2Space α] [LocallyCompactSpace α] [HasNoIsolatedPoints α] +variable [MulAction G α] [LocallyDense G α] [ContinuousMulAction G α] + -- 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 α] +lemma proposition_3_2_subset {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 := @@ -378,9 +407,7 @@ by /-- ## 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 α] : +theorem isBasis : TopologicalSpace.IsTopologicalBasis (RegularSupportBasis.asSet α) := by apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds @@ -393,22 +420,43 @@ by } 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 + 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 α)} + use {HomeoGroup.fromContinuous α g} 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 +-- example (p : α): ∃ (S : Set α), S ∈ (RegularSupportBasis.asSet α) ∧ IsCompact (closure S) ∧ p ∈ S := +-- by +-- have h₁ := TopologicalSpace.IsTopologicalBasis.nhds_hasBasis (isBasis G α) (a := p) +-- have h₂ := compact_basis_nhds p + +-- rw [Filter.hasBasis_iff] at h₁ +-- rw [Filter.hasBasis_iff] at h₂ + +-- have T : Set α := sorry +-- have T_in_nhds : T ∈ 𝓝 p := sorry + +-- let ⟨U, ⟨⟨U_in_nhds, U_compact⟩, U_ss_T⟩⟩ := (h₂ T).mp T_in_nhds +-- let ⟨V, ⟨⟨V_in_basis, p_in_V⟩, V_ss_T⟩⟩ := (h₁ U).mp U_in_nhds + +-- use V +-- (repeat' apply And.intro) <;> try assumption +-- -- apply IsCompact.of_isClosed_subset + +-- -- · assumption +-- -- · sorry +-- -- · assumption +-- sorry + end Basis end RegularSupportBasis end Rubin