This file contains (AI generated) lemmas to help show the αᵢ properties are preserved by homeomorphisms.

theorem PiBase.AlphaTransport.mem_range_symm_comp {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (f : ℕ → Y) (w : X) : w ∈ Set.range (⇑φ.symm ∘ f) ↔ φ w ∈ Set.range f

theorem PiBase.AlphaTransport.mem_range_comp {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (g : ℕ → X) (z : Y) : z ∈ Set.range (⇑φ ∘ g) ↔ φ.symm z ∈ Set.range g

theorem PiBase.AlphaTransport.tendsto_symm_comp {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) {f : ℕ → Y} {y : Y} (hf : Filter.Tendsto f Filter.atTop (nhds y)) : Filter.Tendsto (⇑φ.symm ∘ f) Filter.atTop (nhds (φ.symm y))

theorem PiBase.AlphaTransport.tendsto_comp_of_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) {g : ℕ → X} {y : Y} (hg : Filter.Tendsto g Filter.atTop (nhds (φ.symm y))) : Filter.Tendsto (⇑φ ∘ g) Filter.atTop (nhds y)

theorem PiBase.AlphaTransport.range_comp_subset {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (f : ℕ → ℕ → Y) (g : ℕ → X) (h : Set.range g ⊆ ⋃ (n : ℕ), Set.range (⇑φ.symm ∘ f n)) : Set.range (⇑φ ∘ g) ⊆ ⋃ (n : ℕ), Set.range (f n)

theorem PiBase.AlphaTransport.symm_image_range_diff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (f : ℕ → Y) (g : ℕ → X) : Set.range (⇑φ.symm ∘ f) \ Set.range g = ⇑φ.symm '' (Set.range f \ Set.range (⇑φ ∘ g))

theorem PiBase.AlphaTransport.finite_diff_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (f : ℕ → Y) (g : ℕ → X) : (Set.range f \ Set.range (⇑φ ∘ g)).Finite ↔ (Set.range (⇑φ.symm ∘ f) \ Set.range g).Finite

theorem PiBase.AlphaTransport.symm_range_inter_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (f₁ f₂ : ℕ → Y) : Set.range (⇑φ.symm ∘ f₁) ∩ Set.range (⇑φ.symm ∘ f₂) = ⇑φ.symm '' (Set.range f₁ ∩ Set.range f₂)

theorem PiBase.AlphaTransport.symm_pairwise_disjoint {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : ℕ → ℕ → Y) (h : Pairwise fun (n m : ℕ) => Set.range (S n) ∩ Set.range (S m) = ∅) : Pairwise fun (n m : ℕ) => Set.range (⇑φ.symm ∘ S n) ∩ Set.range (⇑φ.symm ∘ S m) = ∅

theorem PiBase.AlphaTransport.infinite_setOf_finite_diff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : ℕ → ℕ → Y) (T : ℕ → X) (h : {n : ℕ | (Set.range (⇑φ.symm ∘ S n) \ Set.range T).Finite}.Infinite) : {n : ℕ | (Set.range (S n) \ Set.range (⇑φ ∘ T)).Finite}.Infinite

theorem PiBase.AlphaTransport.symm_image_range_inter {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (f : ℕ → Y) (g : ℕ → X) : Set.range (⇑φ.symm ∘ f) ∩ Set.range g = ⇑φ.symm '' (Set.range f ∩ Set.range (⇑φ ∘ g))

theorem PiBase.AlphaTransport.infinite_inter_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (f : ℕ → Y) (g : ℕ → X) : (Set.range f ∩ Set.range (⇑φ ∘ g)).Infinite ↔ (Set.range (⇑φ.symm ∘ f) ∩ Set.range g).Infinite

theorem PiBase.AlphaTransport.infinite_setOf_infinite_inter {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : ℕ → ℕ → Y) (T : ℕ → X) (h : {n : ℕ | (Set.range (⇑φ.symm ∘ S n) ∩ Set.range T).Infinite}.Infinite) : {n : ℕ | (Set.range (S n) ∩ Set.range (⇑φ ∘ T)).Infinite}.Infinite

theorem PiBase.AlphaTransport.nonempty_inter_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (f : ℕ → Y) (g : ℕ → X) : (Set.range f ∩ Set.range (⇑φ ∘ g)).Nonempty ↔ (Set.range (⇑φ.symm ∘ f) ∩ Set.range g).Nonempty

theorem PiBase.AlphaTransport.infinite_setOf_nonempty_inter {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : ℕ → ℕ → Y) (T : ℕ → X) (h : {n : ℕ | (Set.range (⇑φ.symm ∘ S n) ∩ Set.range T).Nonempty}.Infinite) : {n : ℕ | (Set.range (S n) ∩ Set.range (⇑φ ∘ T)).Nonempty}.Infinite