def RestrictedProduct.XS {ι : Type u_1} (X : ι → Type u_2) (U : (i : ι) → Set (X i)) (S : Finset ι) : Set ((i : ι) → X i)

theorem RestrictedProduct.XS_mono {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) (U : (i : ι) → Set (X i)) {S T : Finset ι} (hST : S ⊆ T) : XS X U S ⊆ XS X U T

theorem RestrictedProduct.mem_XS_of_restricted {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) (U : (i : ι) → Set (X i)) (x : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite) : ∃ (S : Finset ι), ⇑x ∈ XS X U S

noncomputable def RestrictedProduct.supportFinset {ι : Type u_1} (X : ι → Type u_2) (U : (i : ι) → Set (X i)) (x : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite) : Finset ι

theorem RestrictedProduct.mem_XS_support {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) (U : (i : ι) → Set (X i)) (x : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite) : ⇑x ∈ XS X U (supportFinset X U x)

theorem RestrictedProduct.XS_mem_restricted {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) (U : (i : ι) → Set (X i)) {S : Finset ι} {x : (i : ι) → X i} (hx : x ∈ XS X U S) : ∀ᶠ (i : ι) in Filter.cofinite, x i ∈ U i

theorem RestrictedProduct.supportFinset_le {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) (U : (i : ι) → Set (X i)) {T : Finset ι} {x : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite} (hx : ⇑x ∈ XS X U T) : supportFinset X U x ⊆ T

def RestrictedProduct.inclusionMap {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) (U : (i : ι) → Set (X i)) {S T : Finset ι} (h : S ⊆ T) : ↑(XS X U S) → ↑(XS X U T)

def RestrictedProduct.transitionMaps {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) (U : (i : ι) → Set (X i)) (S T : Finset ι) : S ≤ T → ↑(XS X U S) → ↑(XS X U T)

@[reducible, inline]

abbrev RestrictedProduct.DirectLimitXS {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) : Type (max u_1 u_2)

theorem RestrictedProduct.cofinite_le_principal_compl {ι : Type u_1} [DecidableEq ι] (S : Finset ι) : Filter.cofinite ≤ Filter.principal (↑S)ᶜ

noncomputable def RestrictedProduct.toDirectLimit {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) (x : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite) : DirectLimitXS X U

noncomputable def RestrictedProduct.fromDirectLimit {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) : DirectLimitXS X U → RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite

theorem RestrictedProduct.fromDirectLimit_toDirectLimit {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) (x : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite) : fromDirectLimit X U (toDirectLimit X U x) = x

theorem RestrictedProduct.toDirectLimit_fromDirectLimit {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) (q : DirectLimitXS X U) : toDirectLimit X U (fromDirectLimit X U q) = q

def RestrictedProduct.toChunk {ι : Type u_1} (X : ι → Type u_2) (U : (i : ι) → Set (X i)) (S : Finset ι) (x : ↑(XS X U S)) : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) (Filter.principal (↑S)ᶜ)

theorem RestrictedProduct.continuous_toChunk {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) (S : Finset ι) : Continuous (toChunk X U S)

theorem RestrictedProduct.continuous_fromDirectLimit {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) : Continuous (fromDirectLimit X U)

theorem RestrictedProduct.inclusion_mem_XS_of_principal {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) {S : Set ι} (hS : Filter.cofinite ≤ Filter.principal S) (y : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) (Filter.principal S)) : ⇑(inclusion X U hS y) ∈ XS X U ⋯.toFinset

theorem RestrictedProduct.continuous_toDirectLimit {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) : Continuous (toDirectLimit X U)

noncomputable def RestrictedProduct.restrictedProduct_homeomorph_directLimit {ι : Type u_1} [DecidableEq ι] (X : ι → Type u_2) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite ≃ₜ DirectLimitXS X U

theorem proposition_25_5 {ι : Type u_2} [DecidableEq ι] (X : ι → Type u_3) [(i : ι) → TopologicalSpace (X i)] (U : (i : ι) → Set (X i)) (hU_open : ∀ (i : ι), IsOpen (U i)) : (∀ (x : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite), ∃ (S : Finset ι), ⇑x ∈ RestrictedProduct.XS X U S) ∧ (∀ {S T : Finset ι}, S ⊆ T → RestrictedProduct.XS X U S ⊆ RestrictedProduct.XS X U T) ∧ (∀ (S : Finset ι), Topology.IsOpenEmbedding (RestrictedProduct.inclusion X U ⋯)) ∧ (∀ {Y : Type u_4} [inst : TopologicalSpace Y] (f : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite → Y), Continuous f ↔ ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S), Continuous (f ∘ RestrictedProduct.inclusion X U hS)) ∧ Nonempty (RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) Filter.cofinite ≃ₜ RestrictedProduct.DirectLimitXS X U)