From 431a2931d75bae9185132cd4362f1330c5be7aaa Mon Sep 17 00:00:00 2001
From: Adrien Burgun <adrien.burgun@orange.fr>
Date: Wed, 27 Dec 2023 22:36:22 +0100
Subject: [PATCH] :sparkles: Implement UltrafilterInBasis.map_basis

---
 Rubin/Filter.lean | 694 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 671 insertions(+), 23 deletions(-)

diff --git a/Rubin/Filter.lean b/Rubin/Filter.lean
index bad2c54..cabfcbf 100644
--- a/Rubin/Filter.lean
+++ b/Rubin/Filter.lean
@@ -3,18 +3,239 @@ import Mathlib.Topology.Basic
 import Mathlib.Topology.Bases
 import Mathlib.Topology.Separation
 
-def Filter.InBasis {α : Type _} (F : Filter α) (B : Set (Set α)) : Prop :=
-  ∀ (S : Set α), S ∈ F → ∃ T ∈ F, T ∈ B ∧ T ⊆ S
+section Order
 
-/--
-This is a formulation for prefilters in a basis that are ultra.
-It is a weaker statement than regular ultrafilters,
-but it allows for some nice properties, like the equivalence of cluster points and neighborhoods.
---/
-structure UltrafilterInBasis {α : Type} (F : Filter α) (B : Set (Set α)) :=
-  in_basis : Filter.InBasis F B
+variable {α β : Type _}
+
+def DoubleMonotoneOn [Preorder α] [Preorder β] (f: α → β) (B : Set α): Prop :=
+  ∀ x, x ∈ B → ∀ y, y ∈ B → (x ≤ y ↔ f x ≤ f y)
+
+variable {f : α → β} {B : Set α}
+
+theorem DoubleMonotoneOn.monotoneOn [Preorder α] [Preorder β] (f_double_mono : DoubleMonotoneOn f B) :
+  MonotoneOn f B :=
+by
+  intro x x_in_B y y_in_B
+  rw [f_double_mono x x_in_B y y_in_B]
+  tauto
+
+theorem DoubleMonotoneOn.injective [PartialOrder α] [Preorder β] (f_double_mono : DoubleMonotoneOn f B) :
+  Function.Injective (Set.restrict B f) :=
+by
+  intro ⟨x, x_in_B⟩ ⟨y, y_in_B⟩
+  simp
+  intro fx_eq_fy
+  apply le_antisymm
+  swap
+  symm at fx_eq_fy
+  all_goals apply le_of_eq at fx_eq_fy
+  all_goals rw [f_double_mono]
+  all_goals assumption
+
+theorem DoubleMonotoneOn.subset_iff {B : Set (Set α)} {f : Set α → Set β} (f_double_mono : DoubleMonotoneOn f B) :
+  ∀ s ∈ B, ∀ t ∈ B, s ⊆ t ↔ f s ⊆ f t :=
+by
+  simp only [<-Set.le_eq_subset]
+  exact f_double_mono
+
+structure OrderIsoOn (α : Type _) (β : Type _) [Preorder α] [Preorder β] (S : Set α) :=
+  toFun : α → β
+  invFun : β → α
+
+  leftInv_on : ∀ a ∈ S, invFun (toFun a) = a
+  rightInv_on : ∀ b ∈ toFun '' S, toFun (invFun b) = b
+
+  toFun_doubleMonotone : DoubleMonotoneOn toFun S
+
+theorem OrderIsoOn.mk_of_subset [Preorder α] [Preorder β] (F : OrderIsoOn α β S)
+  {T : Set α} (T_ss_S : T ⊆ S) : OrderIsoOn α β T
+where
+  toFun := F.toFun
+  invFun := F.invFun
+
+  leftInv_on := by
+    intro a a_in_T
+    rw [F.leftInv_on a (T_ss_S a_in_T)]
+
+  rightInv_on := by
+    intro b b_in_mT
+    have b_in_mS : b ∈ F.toFun '' S := Set.image_subset _ T_ss_S b_in_mT
+    rw [F.rightInv_on b b_in_mS]
+
+  toFun_doubleMonotone := by
+    intro a a_in_T b b_in_T
+    rw [F.toFun_doubleMonotone a (T_ss_S a_in_T) b (T_ss_S b_in_T)]
+
+theorem OrderIsoOn.invFun_doubleMonotone [Preorder α] [Preorder β] (F : OrderIsoOn α β S) :
+  DoubleMonotoneOn F.invFun (F.toFun '' S) :=
+by
+  intro x ⟨x', x'_in_S, x_eq⟩ y ⟨y', y'_in_S, y_eq⟩
+  rw [<-x_eq, <-y_eq]
+  (repeat rw [F.leftInv_on]) <;> try assumption
+  symm
+  apply toFun_doubleMonotone <;> assumption
+
+instance [Preorder α] [Preorder β] : CoeOut (OrderIsoOn α β S) (α → β) where
+  coe := fun F x => F.toFun x
+
+variable [Preorder α] [Preorder β]
+
+theorem OrderIsoOn.toFun_injective (F : OrderIsoOn α β S) :
+  Function.Injective (Set.restrict S F.toFun) :=
+by
+  intro ⟨x, x_in_S⟩ ⟨y, y_in_S⟩
+  simp
+  intro fX_eq_fY
+  rw [<-F.leftInv_on _ x_in_S]
+  rw [<-F.leftInv_on _ y_in_S]
+  rw [fX_eq_fY]
+
+theorem OrderIsoOn.toFun_inj (F : OrderIsoOn α β S) :
+  ∀ x ∈ S, ∀ y ∈ S, F.toFun x = F.toFun y → x = y :=
+by
+  intro x xs y ys fx_eq_fy
+  have res := F.toFun_injective (by
+    show Set.restrict S F.toFun ⟨x, xs⟩ = Set.restrict S F.toFun ⟨y, ys⟩
+    simp
+    exact fx_eq_fy
+  )
+  simp at res
+  exact res
+
+theorem OrderIsoOn.mem_toFun_image (F : OrderIsoOn α β S) (y : β):
+  y ∈ F.toFun '' S → F.invFun y ∈ S :=
+by
+  simp
+  intro x x_in_S y_eq
+  rw [<-y_eq]
+  rw [F.leftInv_on x x_in_S]
+  assumption
+
+theorem OrderIsoOn.toFun_eq_to_invFun (F : OrderIsoOn α β S) :
+  ∀ x ∈ S, ∀ y, F.toFun x = y → x = F.invFun y :=
+by
+  intro x x_in_S y y_eq
+  have y_in_mS : y ∈ F.toFun '' S := by use x
+  rw [<-F.rightInv_on y y_in_mS] at y_eq
+  apply F.toFun_inj <;> try assumption
+  apply mem_toFun_image
+  assumption
 
-  ultra : ∀ (F' : Filter α), F'.InBasis B → F'.NeBot → F' ≤ F → F ≤ F'
+theorem OrderIsoOn.toFun_eq_iff (F : OrderIsoOn α β S) :
+  ∀ x ∈ S, ∀ y ∈ F.toFun '' S, F.toFun x = y ↔ x = F.invFun y :=
+by
+  intro x x_in_S y y_in_fS
+  constructor
+  · apply toFun_eq_to_invFun
+    assumption
+  · intro x_eq
+    rw [x_eq]
+    apply F.rightInv_on
+    assumption
+
+@[simp]
+theorem OrderIsoOn.leftInv_image (F : OrderIsoOn α β S) :
+  (F.invFun ∘ F.toFun) '' S = S :=
+by
+  ext x
+  simp
+  constructor
+  · intro ⟨y, y_in_S, y_eq⟩
+    rw [F.leftInv_on y y_in_S] at y_eq
+    exact y_eq ▸ y_in_S
+  · intro x_in_S
+    use x
+    exact ⟨x_in_S, F.leftInv_on x x_in_S⟩
+
+@[simp]
+theorem OrderIsoOn.leftInv_image' (F : OrderIsoOn α β S) :
+  F.invFun '' (F.toFun '' S) = S := by rw [Set.image_image, <-Function.comp_def, leftInv_image]
+
+def OrderIsoOn.comp {γ : Type _} [Preorder γ] (F : OrderIsoOn α β S)
+  (G : OrderIsoOn β γ (F.toFun '' S)) : OrderIsoOn α γ S where
+  toFun := G.toFun ∘ F.toFun
+  invFun := F.invFun ∘ G.invFun
+
+  leftInv_on := by
+    intro x x_in_S
+    simp
+    rw [G.leftInv_on _ (by use x)]
+    rw [F.leftInv_on x x_in_S]
+
+  rightInv_on := by
+    intro y y_in_img
+    simp
+    rw [Function.comp_def, <-Set.image_image G.toFun F.toFun] at y_in_img
+    let ⟨z, z_in_fS, fz_eq_y⟩ := y_in_img
+    have z_eq_fy : z = G.invFun y := G.toFun_eq_to_invFun z z_in_fS y fz_eq_y
+    rw [<-z_eq_fy, <-fz_eq_y]
+    rw [F.rightInv_on]
+    assumption
+
+  toFun_doubleMonotone := by
+    intro x x_in_S y y_in_S
+    simp
+    apply Iff.trans
+    exact F.toFun_doubleMonotone x x_in_S y y_in_S
+    apply G.toFun_doubleMonotone
+    use x
+    use y
+
+@[simp]
+theorem OrderIsoOn.comp_toFun {γ : Type _} [Preorder γ] (F : OrderIsoOn α β S) (G : OrderIsoOn β γ (F.toFun '' S)) :
+  (F.comp G).toFun = G.toFun ∘ F.toFun := rfl
+
+def OrderIsoOn.inv (F : OrderIsoOn α β S) : OrderIsoOn β α (F.toFun '' S) where
+  toFun := F.invFun
+  invFun := F.toFun
+
+  leftInv_on := F.rightInv_on
+  rightInv_on := by
+    simp
+    exact F.leftInv_on
+
+  toFun_doubleMonotone := F.invFun_doubleMonotone
+
+@[simp]
+theorem OrderIsoOn.inv_toFun (F : OrderIsoOn α β S) : F.inv.toFun = F.invFun := rfl
+
+@[simp]
+theorem OrderIsoOn.inv_invFun (F : OrderIsoOn α β S) : F.inv.invFun = F.toFun := rfl
+
+def OrderIso.orderIsoOn (F : α ≃o β) (S : Set α) : OrderIsoOn α β S where
+  toFun := F.toFun
+  invFun := F.invFun
+
+  leftInv_on := by
+    intro a _
+    apply Equiv.left_inv
+  rightInv_on := by
+    intro b _
+    apply Equiv.right_inv
+
+  toFun_doubleMonotone := by
+    intro a _ b _
+    exact Iff.symm (RelIso.map_rel_iff F)
+
+instance : Coe (α ≃o β) (OrderIsoOn α β S) where
+  coe := fun f => OrderIso.orderIsoOn f S
+
+def OrderIsoOn.identity (α : Type _) [Preorder α] (S : Set α) : OrderIsoOn α α S where
+  toFun := id
+  invFun := id
+  leftInv_on := by simp
+  rightInv_on := by simp
+  toFun_doubleMonotone := by simp [DoubleMonotoneOn]
+
+@[simp]
+theorem OrderIsoOn.comp_inv (F : OrderIsoOn α β S) : ∀ x ∈ S, (F.comp (F.inv)).toFun x = x := by
+  simp
+  exact F.leftInv_on
+
+end Order
+
+def Filter.InBasis {α : Type _} (F : Filter α) (B : Set (Set α)) : Prop :=
+  ∀ (S : Set α), S ∈ F → ∃ T ∈ F, T ∈ B ∧ T ⊆ S
 
 theorem Filter.InBasis.from_hasBasis {α ι : Type _} {F : Filter α} {pi : ι → Prop} {si : ι → Set α}
   (F_basis: Filter.HasBasis F pi si)
@@ -71,13 +292,29 @@ by
   · intro ⟨S, S_in_F, _, S_ss_T⟩
     exact mem_of_superset S_in_F S_ss_T
 
---  (map_mono : ∀ A B : Set α, A ⊆ B ↔ map A ⊆ map B) (F_basis : F.InBasis B)
+theorem Filter.InBasis.mem_image_basis_of_injective_on (F : Filter α) (B : Set (Set α))
+  {f : Set α → Set β} (f_injective_on : Function.Injective (Set.restrict B f))
+  {S : Set α} (S_in_B : S ∈ B) : f S ∈ f '' (basis F B) ↔ S ∈ basis F B :=
+by
+  simp
+  constructor
+  · intro ⟨T, T_in_basis, fT_eq_fS⟩
+    have T_eq_S : (⟨T, T_in_basis.right⟩ : { s // s ∈ B }) = ⟨S, S_in_B⟩ := by
+      apply f_injective_on
+      simp
+      exact fT_eq_fS
+    simp at T_eq_S
+    rw [<-T_eq_S]
+    assumption
+  · intro S_in_basis
+    use S
+
 def Filter.InBasis.map_basis {α β : Type _} (F : Filter α) (B : Set (Set α))
   (map : Set α → Set β): Filter β :=
   ⨅ (S : Filter.InBasis.basis F B), Filter.principal (map S)
 
 lemma Filter.InBasis.map_directed {β : Type _} (F_basis : F.InBasis B)
-  (map : Set α → Set β) (map_mono : Monotone map) :
+  (map : Set α → Set β) (map_mono : MonotoneOn map B) :
   Directed (fun S T => S ≥ T) fun S : Filter.InBasis.basis F B => Filter.principal (map S.val) :=
 by
   intro ⟨S, S_in_F, S_in_B⟩ ⟨T, T_in_F, T_in_B⟩
@@ -89,7 +326,7 @@ by
   constructor <;> apply map_mono <;> assumption
 
 theorem Filter.InBasis.map_basis_neBot {β : Type _} [Nonempty β] (F_basis : F.InBasis B)
-  (map : Set α → Set β) (map_mono : Monotone map) (map_nonempty : ∀ S ∈ B, Set.Nonempty (map S)) :
+  (map : Set α → Set β) (map_mono : MonotoneOn map B) (map_nonempty : ∀ S ∈ B, Set.Nonempty (map S)) :
   Filter.NeBot (Filter.InBasis.map_basis F B map) :=
 by
   apply Filter.iInf_neBot_of_directed
@@ -98,8 +335,18 @@ by
     simp
     exact map_nonempty _ S_in_B
 
-theorem Filter.InBasis.map_basis_hasBasis {β : Type _} [Nonempty β] (F_basis : F.InBasis B)
-  (map : Set α → Set β) (map_mono : Monotone map):
+theorem Filter.InBasis.map_basis_neBot_of_neBot {β : Type _} [Nonempty β] [Filter.NeBot F] (F_basis : F.InBasis B)
+  (map : Set α → Set β) (map_mono : MonotoneOn map B) (map_nonempty : ∀ S ∈ B, S.Nonempty → Set.Nonempty (map S)) :
+  Filter.NeBot (Filter.InBasis.map_basis F B map) :=
+by
+  apply Filter.iInf_neBot_of_directed
+  · exact Filter.InBasis.map_directed F_basis map map_mono
+  · intro ⟨S, S_in_F, S_in_B⟩
+    simp
+    exact map_nonempty _ S_in_B (nonempty_of_mem S_in_F)
+
+theorem Filter.InBasis.map_basis_hasBasis {β : Type _} (F_basis : F.InBasis B)
+  (map : Set α → Set β) (map_mono : MonotoneOn map B):
   (Filter.InBasis.map_basis F B map).HasBasis (fun T : Set α => T ∈ F ∧ T ∈ B) map :=
 by
   unfold map_basis
@@ -113,16 +360,11 @@ by
   · exact Filter.InBasis.map_directed F_basis map map_mono
 
 theorem Filter.InBasis.map_basis_inBasis (F_basis : Filter.InBasis F B)
-  (map : Set α → Set β) (map_mono : Monotone map) (map_nonempty : ∀ S ∈ B, Set.Nonempty (map S)) :
+  (map : Set α → Set β) (map_mono : MonotoneOn map B) :
   (Filter.InBasis.map_basis F B map).InBasis (map '' B) :=
 by
   intro S S_in_map
 
-  have β_nonempty : Nonempty β := by
-    let ⟨T, _, T_in_B⟩ := Filter.InBasis.basis_nonempty' F_basis
-    let ⟨x, _⟩ := map_nonempty T T_in_B
-    use x
-
   have has_basis := Filter.InBasis.map_basis_hasBasis F_basis map map_mono
 
   rw [has_basis.mem_iff'] at S_in_map
@@ -136,10 +378,285 @@ by
     use T
   · assumption
 
+theorem Filter.InBasis.map_basis_id (F_basis : F.InBasis B) (f : Set α → Set α) (f_idlike : ∀ S ∈ B, f S = S):
+  Filter.InBasis.map_basis F B f = F :=
+by
+  simp [map_basis]
+  ext S
+  have basis_nonempty := Filter.InBasis.basis_nonempty' F_basis
+  have basis_directed := Filter.InBasis.map_directed F_basis id (monotone_id.monotoneOn B)
+  simp only [id_eq] at basis_directed
+
+  conv => {
+    lhs
+    rhs
+    congr; intro x
+    rw [f_idlike _ x.prop.right]
+  }
+
+  rw [mem_iInf_of_directed basis_directed]
+  rw [(F_basis.basis_hasBasis).mem_iff]
+  simp
+
+theorem Filter.InBasis.mem_map_basis
+  (map : Set α → Set β) (map_mono : MonotoneOn map B)
+  (F_basis : Filter.InBasis F B) (x : Set β) :
+  x ∈ (Filter.InBasis.map_basis F B map) ↔ ∃ y : Set α, y ∈ F ∧ y ∈ B ∧ map y ⊆ x :=
+by
+  rw [(Filter.InBasis.map_basis_hasBasis F_basis map map_mono).mem_iff]
+  simp only [and_assoc]
+
 theorem nhds_in_basis [TopologicalSpace α] (p : α) (B_basis : TopologicalSpace.IsTopologicalBasis B):
   (nhds p).InBasis B :=
   Filter.InBasis.from_hasBasis B_basis.nhds_hasBasis (fun _ ⟨in_B, _⟩ => in_B)
 
+theorem Filter.InBasis.basis_map_basis (map : Set α → Set β)
+  (map_double_mono : DoubleMonotoneOn map B) {F : Filter α} (F_basis : F.InBasis B):
+  Filter.InBasis.basis (Filter.InBasis.map_basis F B map) (map '' B) = map '' (Filter.InBasis.basis F B) :=
+by
+  ext x
+  simp [basis]
+  rw [Filter.InBasis.mem_map_basis map map_double_mono.monotoneOn F_basis]
+  constructor
+  · intro ⟨⟨y1, y1_in_F, _, y1_ss_x⟩, ⟨y2, y2_in_B, y2_eq⟩⟩
+    use y2
+    rw [<-y2_eq] at y1_ss_x
+    repeat' apply And.intro
+    apply Filter.mem_of_superset y1_in_F
+    rw [map_double_mono.subset_iff]
+    all_goals assumption
+  · intro ⟨S, ⟨S_in_F, S_in_B⟩, x_eq⟩
+    constructor
+    all_goals use S
+    repeat' apply And.intro
+    any_goals apply subset_of_eq
+    all_goals assumption
+
+theorem Filter.InBasis.mem_basis_iff_of_basis_set (F : Filter α) {S : Set α} (S_in_B : S ∈ B):
+  S ∈ basis F B ↔ S ∈ F :=
+by
+  unfold basis
+  simp
+  tauto
+
+theorem Filter.InBasis.map_mem_map_basis_of_basis_set (map : Set α → Set β) (map_double_mono : DoubleMonotoneOn map B)
+  {F : Filter α} (F_basis : F.InBasis B) {S : Set α} (S_in_B : S ∈ B):
+  map S ∈ Filter.InBasis.map_basis F B map ↔ S ∈ F :=
+by
+  suffices S ∈ basis F B ↔ map S ∈ map '' (basis F B) by
+    rw [mem_basis_iff_of_basis_set _ S_in_B] at this
+    rw [this]
+    have mS_in_mB : map S ∈ map '' B := by
+      simp
+      use S
+    rw [<-basis_map_basis map map_double_mono F_basis]
+    rw [mem_basis_iff_of_basis_set _ mS_in_mB]
+
+  rw [Filter.InBasis.mem_image_basis_of_injective_on _ _ map_double_mono.injective S_in_B]
+
+-- TODO: clean this up :c
+theorem Filter.InBasis.map_basis_comp {γ : Type _} (m₁ : OrderIsoOn (Set α) (Set β) B)
+  (m₂ : OrderIsoOn (Set β) (Set γ) (m₁.toFun '' B))
+  {F : Filter α} (F_basis : F.InBasis B):
+  Filter.InBasis.map_basis (Filter.InBasis.map_basis F B m₁) (m₁.toFun '' B) m₂.toFun = Filter.InBasis.map_basis F B (m₁.comp m₂).toFun :=
+by
+
+  unfold map_basis
+  rw [iInf_subtype]
+  simp [basis_map_basis]
+  rw [<-iInf_subtype (f := fun i => Filter.principal (m₂.toFun i.val))]
+
+  have F'_basis := (Filter.InBasis.map_basis_inBasis F_basis m₁.toFun m₁.toFun_doubleMonotone.monotoneOn)
+  have basis_nonempty : Nonempty { i // i ∈ basis (⨅ S : basis F B, Filter.principal (m₁.toFun ↑S)) (m₁.toFun '' B) } :=
+    (Filter.InBasis.basis_nonempty' F'_basis).elim (fun p => ⟨p.val, p.prop⟩)
+
+  have basis_nonempty' := Filter.InBasis.basis_nonempty' F_basis
+
+  have m₁_directed := Filter.InBasis.map_directed F_basis m₁.toFun m₁.toFun_doubleMonotone.monotoneOn
+  have m₂_directed := Filter.InBasis.map_directed F'_basis m₂.toFun m₂.toFun_doubleMonotone.monotoneOn
+
+  have m₁₂_directed := Filter.InBasis.map_directed F_basis (m₁.comp m₂).toFun (m₁.comp m₂).toFun_doubleMonotone.monotoneOn
+  simp only [OrderIsoOn.comp_toFun, Function.comp_apply] at m₁₂_directed
+
+  ext S
+  rw [mem_iInf_of_directed]
+  swap
+  assumption
+
+  constructor
+  · intro ⟨⟨T, ⟨T_in_basis, T_in_m₁B⟩⟩, m₂T_ss_S⟩
+    simp at m₂T_ss_S
+    apply Filter.mem_of_superset _ m₂T_ss_S
+    rw [mem_iInf_of_directed]
+    rw [mem_iInf_of_directed] at T_in_basis
+    any_goals assumption
+
+    let ⟨⟨U, ⟨U_in_F, U_in_B⟩⟩, m₁U_ss_T⟩ := T_in_basis
+    simp at m₁U_ss_T
+    use ⟨U, ⟨U_in_F, U_in_B⟩⟩
+
+    simp
+    apply m₂.toFun_doubleMonotone.monotoneOn
+    use U
+    all_goals assumption
+  · intro S_in_iInf
+    rw [mem_iInf_of_directed] at S_in_iInf
+    any_goals assumption
+    let ⟨⟨U, ⟨U_in_F, U_in_B⟩⟩, m₁₂U_ss_S⟩ := S_in_iInf
+    simp at m₁₂U_ss_S
+
+    have m₁U_in_basis : m₁.toFun U ∈ basis (map_basis F B m₁.toFun) (m₁.toFun '' B) := by
+      constructor
+      swap
+      use U
+      rw [map_mem_map_basis_of_basis_set m₁.toFun m₁.toFun_doubleMonotone]
+      all_goals assumption
+
+    use ⟨m₁.toFun U, m₁U_in_basis⟩
+    assumption
+
+theorem Filter.InBasis.map_basis_inv (map : OrderIsoOn (Set α) (Set β) B)
+  {F : Filter α} (F_basis : F.InBasis B):
+  Filter.InBasis.map_basis (Filter.InBasis.map_basis F B map) (map.toFun '' B) map.invFun = F :=
+by
+  rw [<-map.inv_toFun, map_basis_comp _ _ F_basis, map_basis_id F_basis]
+  exact OrderIsoOn.comp_inv map
+
+theorem Filter.InBasis.map_basis_inv' (map : OrderIsoOn (Set α) (Set β) B)
+  {F : Filter β} (F_basis : F.InBasis (map.toFun '' B)):
+  Filter.InBasis.map_basis (Filter.InBasis.map_basis F (map.toFun '' B) map.invFun) B map.toFun = F :=
+by
+  nth_rw 4 [<-OrderIsoOn.leftInv_image' map]
+  rw [<-map.inv_toFun]
+  nth_rw 5 [<-map.inv_invFun]
+  rw [<-map.inv.inv_toFun]
+
+  rw [map_basis_comp map.inv map.inv.inv F_basis, map_basis_id F_basis]
+
+  simp
+  intro a a_in_B
+  rw [map.leftInv_on a a_in_B]
+
+
+theorem Filter.InBasis.map_basis_mono (map : OrderIsoOn (Set α) (Set β) B)
+  {F G : Filter α} (F_basis : F.InBasis B) (G_basis : G.InBasis B):
+  Filter.InBasis.map_basis F B map.toFun ≤ Filter.InBasis.map_basis G B map.toFun → F ≤ G :=
+by
+  intro mF_le_mG S S_in_G
+  let ⟨T, T_in_G, T_in_B, T_ss_S⟩ := G_basis S S_in_G
+  have mT_in_mG : map.toFun T ∈ map_basis G B map.toFun := by
+    rw [map_mem_map_basis_of_basis_set map.toFun map.toFun_doubleMonotone]
+    all_goals assumption
+  have mT_in_mF := mF_le_mG mT_in_mG
+  rw [map_mem_map_basis_of_basis_set map.toFun map.toFun_doubleMonotone] at mT_in_mF
+  apply Filter.mem_of_superset mT_in_mF
+  all_goals assumption
+
+theorem Filter.InBasis.map_basis_le_iff (map : OrderIsoOn (Set α) (Set β) B)
+  {F G : Filter α} (F_basis : F.InBasis B) (G_basis : G.InBasis B):
+  Filter.InBasis.map_basis F B map.toFun ≤ Filter.InBasis.map_basis G B map.toFun ↔ F ≤ G :=
+by
+  constructor
+  · exact map_basis_mono map F_basis G_basis
+  · nth_rw 1 [<-map_basis_inv map F_basis]
+    nth_rw 1 [<-map_basis_inv map G_basis]
+    rw [<-OrderIsoOn.inv_toFun]
+    apply map_basis_mono
+    all_goals apply map_basis_inBasis
+    any_goals assumption
+    all_goals exact map.toFun_doubleMonotone.monotoneOn
+
+theorem Filter.InBasis.map_basis_inBasis' (map : OrderIsoOn (Set α) (Set β) B)
+  {F : Filter α} (F_basis : F.InBasis B) :
+  (Filter.InBasis.map_basis F B map.toFun).InBasis (map.toFun '' B) :=
+by
+  apply map_basis_inBasis
+  assumption
+  exact map.toFun_doubleMonotone.monotoneOn
+
+theorem Filter.InBasis.map_basis_inBasis₂ (map : OrderIsoOn (Set α) (Set β) B)
+  {F : Filter β} (F_basis : F.InBasis (map.toFun '' B)) :
+  (Filter.InBasis.map_basis F (map.toFun '' B) map.invFun).InBasis B :=
+by
+  nth_rw 4 [<-OrderIsoOn.leftInv_image map]
+  rw [Function.comp_def, <-Set.image_image map.invFun]
+  apply map_basis_inBasis
+  assumption
+  exact map.invFun_doubleMonotone.monotoneOn
+
+theorem Filter.InBasis.map_basis_le_inv (map : OrderIsoOn (Set α) (Set β) B)
+  {F : Filter α} (F_basis : F.InBasis B) {G : Filter β} (G_basis : G.InBasis (map.toFun '' B)) :
+  F ≤ Filter.InBasis.map_basis G (map.toFun '' B) map.invFun ↔ Filter.InBasis.map_basis F B map.toFun ≤ G :=
+by
+  suffices ∀ map : OrderIsoOn (Set α) (Set β) B, ∀ F : Filter α, F.InBasis B → ∀ G : Filter β, G.InBasis (map.toFun '' B) →
+    F ≤ Filter.InBasis.map_basis G (map.toFun '' B) map.invFun →
+    Filter.InBasis.map_basis F B map.toFun ≤ G
+  by
+    constructor
+    · apply this
+      all_goals assumption
+    · intro mF_le_G
+
+      nth_rw 1 [<-map_basis_inv map F_basis]
+      apply map_basis_mono map
+      rw [map_basis_inv _ F_basis]
+      any_goals assumption
+      apply map_basis_inBasis₂
+      assumption
+
+      apply this
+      rw [map_basis_inv _ F_basis]
+      assumption
+      apply map_basis_inBasis'
+      apply map_basis_inBasis₂
+      assumption
+
+      rw [<-OrderIsoOn.inv_toFun, map_basis_le_iff]
+
+      · simp
+        rw [map_basis_inv']
+        exact mF_le_G
+        assumption
+      · apply map_basis_inBasis'
+        assumption
+      · simp
+        rw [map_basis_inv']
+        all_goals assumption
+
+  intro map F F_basis G G_basis F_le_mG
+  intro S S_in_G
+  let ⟨T, T_in_G, T_in_mB, T_ss_S⟩ := G_basis S S_in_G
+  let ⟨U, U_in_B, T_eq⟩ := T_in_mB
+  have mT_in_F : map.invFun T ∈ F := by
+    apply F_le_mG
+    rw [map_mem_map_basis_of_basis_set]
+    any_goals assumption
+    exact map.invFun_doubleMonotone
+  have U_in_F : U ∈ F := by
+    rw [<-T_eq] at mT_in_F
+    rw [map.leftInv_on U U_in_B] at mT_in_F
+    exact mT_in_F
+
+  apply Filter.mem_of_superset
+  · show map.toFun U ∈ map_basis F B map.toFun
+    rw [map_mem_map_basis_of_basis_set]
+    any_goals assumption
+    exact map.toFun_doubleMonotone
+  · rw [T_eq]
+    assumption
+
+theorem Filter.InBasis.map_basis_le_inv' (map : OrderIsoOn (Set α) (Set β) B)
+  {F : Filter α} (F_basis : F.InBasis B) {G : Filter β} (G_basis : G.InBasis (map.toFun '' B)) :
+  G ≤ Filter.InBasis.map_basis F B map.toFun ↔ Filter.InBasis.map_basis G (map.toFun '' B) map.invFun ≤ F :=
+by
+  nth_rw 1 [<-map.leftInv_image']
+  rw [<-map.inv_invFun, <-map.inv_toFun]
+
+  rw [<-map.leftInv_image', <-map.inv_toFun] at F_basis
+  nth_rw 1 [map.inv_invFun]
+  rw [Filter.InBasis.map_basis_le_inv _ G_basis F_basis]
+  simp
+
 instance Filter.InBasis.order_bot : OrderBot { F : Filter α // F.InBasis B ∨ F = ⊥ } where
   bot := ⟨⊥, by right; rfl ⟩
   bot_le := by
@@ -296,7 +813,8 @@ by
 
 theorem Filter.InBasis.is_atomic
   (basis_closed : ∀ b1 b2 : Set α, b1 ∈ B → b2 ∈ B → Set.Nonempty (b1 ∩ b2) → b1 ∩ b2 ∈ B)
-  : IsAtomic { F : Filter α // F.InBasis B ∨ F = ⊥ } := by
+  : IsAtomic { F : Filter α // F.InBasis B ∨ F = ⊥ } :=
+by
   by_cases α_nonempty? : Nonempty α
   swap
   {
@@ -375,4 +893,134 @@ theorem Filter.InBasis.is_atomic
   simp
   use F_basis
 
--- TODO: define UltrafilterInBasis.of :)
+/--
+This is a formulation for prefilters in a basis that are ultra.
+It is a weaker statement than regular ultrafilters,
+but it allows for some nice properties, like the equivalence of cluster points and neighborhoods.
+--/
+structure UltrafilterInBasis {α : Type} (B : Set (Set α)) :=
+  filter : Filter α
+
+  in_basis : Filter.InBasis filter B
+
+  ne_bot : Filter.NeBot filter
+
+  ultra : ∀ (F' : Filter α), F'.InBasis B → F'.NeBot → F' ≤ filter → filter ≤ F'
+
+instance : CoeOut (@UltrafilterInBasis α B) (Filter α) where
+  coe := fun U => U.filter
+
+instance : Membership (Set α) (UltrafilterInBasis B) where
+  mem := fun s U => s ∈ U.filter
+
+instance (U : UltrafilterInBasis B): Filter.NeBot (U.filter) where
+  ne' := U.ne_bot.ne
+
+theorem UltrafilterInBasis.exists_le {α: Type _} {F : Filter α} {B : Set (Set α)}
+  (basis_closed : ∀ b1 b2 : Set α, b1 ∈ B → b2 ∈ B → Set.Nonempty (b1 ∩ b2) → b1 ∩ b2 ∈ B)
+  (F_basis : Filter.InBasis F B) (F_nebot : Filter.NeBot F) :
+  ∃ U : UltrafilterInBasis B, U.filter ≤ F :=
+by
+  have atomic := Filter.InBasis.is_atomic basis_closed
+  let ⟨⟨U, U_basis⟩, U_atom, U_le_F⟩ := (atomic.eq_bot_or_exists_atom_le ⟨F, Or.intro_left _ F_basis⟩).resolve_left (by simp; exact F_nebot.ne)
+
+  have U_neBot : Filter.NeBot U := by
+    constructor
+    have U_atom := U_atom.left
+    simp at U_atom
+    exact U_atom
+
+  have U_basis := U_basis.resolve_right U_neBot.ne
+
+  simp at U_le_F
+
+  have U_ultra : ∀ (F' : Filter α), F'.InBasis B → F'.NeBot → F' ≤ U → U ≤ F' := by
+    intro F' F'_basis F'_neBot F'_le
+    have U_atom := U_atom.right
+    simp at U_atom
+    cases le_iff_lt_or_eq.mp F'_le with
+    | inl F'_lt_U =>
+      exfalso
+      apply F'_neBot.ne
+      apply U_atom
+      left
+      all_goals assumption
+    | inr F'_eq_U =>
+      symm at F'_eq_U
+      exact le_of_eq F'_eq_U
+
+  use ⟨U, U_basis, U_neBot, U_ultra⟩
+
+noncomputable def UltrafilterInBasis.of {α: Type _} {F : Filter α} {B : Set (Set α)}
+  (basis_closed : ∀ b1 b2 : Set α, b1 ∈ B → b2 ∈ B → Set.Nonempty (b1 ∩ b2) → b1 ∩ b2 ∈ B)
+  (F_basis : Filter.InBasis F B) [F_neBot : Filter.NeBot F]:
+  UltrafilterInBasis B := Exists.choose $ UltrafilterInBasis.exists_le basis_closed F_basis F_neBot
+
+theorem UltrafilterInBasis.of_le {α: Type _} {F : Filter α} {B : Set (Set α)}
+  (basis_closed : ∀ b1 b2 : Set α, b1 ∈ B → b2 ∈ B → Set.Nonempty (b1 ∩ b2) → b1 ∩ b2 ∈ B)
+  (F_basis : Filter.InBasis F B) [F_neBot : Filter.NeBot F]:
+  UltrafilterInBasis.of basis_closed F_basis ≤ F :=
+by
+  exact Exists.choose_spec $ UltrafilterInBasis.exists_le basis_closed F_basis F_neBot
+
+theorem UltrafilterInBasis.coe_in_basis (U : UltrafilterInBasis B) : Filter.InBasis U B := U.in_basis
+
+theorem UltrafilterInBasis.map_basis_ultra [Nonempty α] {β : Type _}
+  (empty_notin_B : ∅ ∉ B)
+  (map : OrderIsoOn (Set α) (Set β) B)
+  (U : UltrafilterInBasis B) :
+  ∀ (F : Filter β), F.InBasis (map.toFun '' B) → F.NeBot →
+  F ≤ Filter.InBasis.map_basis U B map → Filter.InBasis.map_basis U B map ≤ F :=
+by
+  intro F F_in_basis F_neBot F_le_map
+  intro S S_in_F
+
+  have U_le_mF : U ≤ Filter.InBasis.map_basis F (map.toFun '' B) map.invFun := by
+    apply U.ultra
+    apply Filter.InBasis.map_basis_inBasis₂
+    · assumption
+    · apply Filter.InBasis.map_basis_neBot_of_neBot F_in_basis
+      exact map.invFun_doubleMonotone.monotoneOn
+      intro S ⟨T, T_in_B, T_eq⟩ _
+      rw [<-T_eq, map.leftInv_on T T_in_B]
+      rw [Set.nonempty_iff_ne_empty]
+      intro T_empty
+      exact empty_notin_B (T_empty ▸ T_in_B)
+    · rw [Filter.InBasis.map_basis_le_inv' map U.in_basis F_in_basis] at F_le_map
+      exact F_le_map
+
+  rw [Filter.InBasis.mem_map_basis map.toFun map.toFun_doubleMonotone.monotoneOn U.in_basis]
+  let ⟨T, T_in_F, T_in_mB, T_ss_S⟩ := F_in_basis S S_in_F
+
+  use map.invFun T
+  repeat' apply And.intro
+  · apply U_le_mF
+    rw [Filter.InBasis.map_mem_map_basis_of_basis_set]
+    any_goals assumption
+    exact map.invFun_doubleMonotone
+  · apply map.mem_toFun_image
+    assumption
+  · rw [map.rightInv_on T T_in_mB]
+    exact T_ss_S
+
+def UltrafilterInBasis.map_basis [Nonempty α] {β : Type _} [Nonempty β]
+  (empty_notin_B : ∅ ∉ B)
+  (map : OrderIsoOn (Set α) (Set β) B)
+  (empty_notin_mB : ∅ ∉ map.toFun '' B)
+  (U : UltrafilterInBasis B) :
+  UltrafilterInBasis (map.toFun '' B)
+where
+  filter := Filter.InBasis.map_basis U.filter B map.toFun
+  in_basis := Filter.InBasis.map_basis_inBasis' map U.in_basis
+  ne_bot := by
+    apply Filter.InBasis.map_basis_neBot_of_neBot U.in_basis _ map.toFun_doubleMonotone.monotoneOn
+    intro S S_in_B _
+    by_contra empty
+    rw [Set.not_nonempty_iff_eq_empty] at empty
+    apply empty_notin_mB
+    use S
+  ultra := by
+    apply map_basis_ultra
+    exact empty_notin_B
+
+-- TODO: show that clusterpt iff le nhds if B is a topological basis