TopologicalSpace.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

48 declarations, 0 contain sorry, 0 declared as axioms

Topological Space

Material destined for Mathlib.

Imports (12)

Imported by 6 files

theorem RestrictedProduct.isOpen_forall_mem_of_eventually_eq line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, TopologicalSpace, IsOpen, Filter.Eventually, Eq, Filter.cofinite, RestrictedProduct, Set.ofPred, Membership.mem
Proof uses: Eq.mpr, Inter.inter, Set, Set.preimage, Set.pi, Compl.compl, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Set.ext, Iff, And, Not, id, congrArg, Eq.trans, congrFun', forall_congr and 22 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem RestrictedProduct.isCompact_forall_mem_of_eventually_subset line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, TopologicalSpace, IsOpen, IsCompact, Filter.Eventually, LE.le, Set, Filter.cofinite, RestrictedProduct, Set.ofPred, Membership.mem
Proof uses: Eq.mpr, Set.image, Filter.principal, RestrictedProduct.inclusion, Iff.mpr, Filter, Filter.le_principal_iff, Set.preimage, Set.pi, Set.univ, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, Set.ext, Iff, Exists, And and 26 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem Continuous.restrictedProduct_congrRight line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, TopologicalSpace, Filter.Eventually, Set.MapsTo, Continuous, RestrictedProduct, RestrictedProduct.map
Proof uses: RestrictedProduct.mapAlong_continuous, id, Filter.tendsto_id
1 instances, coercions and auxiliary constants left out.
def ContinuousMulEquiv.restrictedProductCongrRight line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, SetLike, Monoid, SubmonoidClass, TopologicalSpace, ContinuousMulEquiv, Filter.Eventually, Set.BijOn, RestrictedProduct
Proof uses: MulEquiv, MulEquiv.restrictedProductCongrRight, ContinuousMulEquiv.toMulEquiv, ContinuousMulEquiv.mk
22 instances, coercions and auxiliary constants left out.
lemma Equiv.continuous_restrictedProductProd The forward direction of Equiv.restrictedProductProd is continuous with any filter, not just the cofinite one line 114 source
Source documentation
The forward direction of Equiv.restrictedProductProd is continuous with any filter, not just the cofinite one

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, TopologicalSpace, Continuous, RestrictedProduct, Prod, SProd.sprod, Equiv, Equiv.restrictedProductProd
Proof uses: id, Continuous.prodMk, RestrictedProduct.map, Prod.fst, Prod.snd, Continuous.restrictedProduct_congrRight, Continuous.fst, continuous_id', Continuous.snd
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma Equiv.continuous_restrictedProductProd
    [∀ i, TopologicalSpace (A i)] [∀ i, TopologicalSpace (B i)] :
    Continuous (Equiv.restrictedProductProd (C := C) (D := D) (ℱ := ℱ)) := by
…
```
Mentions: Equiv.restrictedProductProd
lemma Equiv.continuous_restrictedProductProd_symm line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, Continuous, Prod, RestrictedProduct, Filter.principal, SProd.sprod, Equiv, Equiv.symm, Equiv.restrictedProductProd
Proof uses: id, Eq.mpr, Equiv.mk, Prod.mk, RestrictedProduct.map, Prod.fst, Prod.snd, Subtype.mk, Filter.Eventually, Membership.mem, Function.comp, Eq, congrArg, propext, RestrictedProduct.continuous_rng_of_principal_iff_forall, And, continuous_prodMk, And.intro, Continuous.comp, RestrictedProduct.continuous_eval and 2 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Homeomorph.restrictedProductProd The homeomorphism between restricted product of binary products, and the binary projuct of the restricted products, when the products are with respect to open subsets line 136 source
Source documentation
The homeomorphism between restricted product of binary products, and the binary projuct of the restricted products, when the products are with respect to open subsets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, IsOpen, Homeomorph, RestrictedProduct, Prod, SProd.sprod, Filter.cofinite
Proof uses: Equiv, Equiv.restrictedProductProd, Homeomorph.mk
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def Homeomorph.restrictedProductProd [∀ i, TopologicalSpace (A i)] [∀ i, TopologicalSpace (B i)]
    (hCopen : ∀ (i : ι), IsOpen (C i)) (hDopen : ∀ (i : ι), IsOpen (D i)) :
    Πʳ i, [A i × B i, C i ×ˢ D i] ≃ₜ (Πʳ i, [A i, C i]) × (Πʳ i, [B i, D i]) where
…
```
lemma Homeomorph.restrictedProductProd_symm_apply_fst line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, IsOpen, Prod, RestrictedProduct, Filter.cofinite, Eq, Prod.fst, SProd.sprod, Homeomorph, Homeomorph.symm, Homeomorph.restrictedProductProd
Proof uses: rfl
14 instances, coercions and auxiliary constants left out.
lemma Homeomorph.restrictedProductProd_symm_apply_snd line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, IsOpen, Prod, RestrictedProduct, Filter.cofinite, Eq, Prod.snd, SProd.sprod, Homeomorph, Homeomorph.symm, Homeomorph.restrictedProductProd
Proof uses: rfl
14 instances, coercions and auxiliary constants left out.
lemma Equiv.continuous_restrictedProductPi The forward direction of Equiv.restrictedProductPi is continuous with any filter, not just the cofinite one line 175 source
Source documentation
The forward direction of Equiv.restrictedProductPi is continuous with any filter, not just the cofinite one

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Fintype, Set, TopologicalSpace, Continuous, RestrictedProduct, Set.ofPred, Membership.mem, Equiv, Equiv.restrictedProductPi
Proof uses: id, continuous_pi, RestrictedProduct.map, Continuous.restrictedProduct_congrRight, continuous_apply
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma Equiv.continuous_restrictedProductPi [∀ j i, TopologicalSpace (A j i)] :
    Continuous (Equiv.restrictedProductPi (C := C) (ℱ := ℱ)) := by
…
```
Mentions: Equiv.restrictedProductPi
lemma Equiv.continuous_restrictedProductPi_symm line 181 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Set, TopologicalSpace, Continuous, RestrictedProduct, Filter.principal, Set.ofPred, Membership.mem, Equiv, Equiv.symm, Equiv.restrictedProductPi
Proof uses: Eq.mpr, Function.comp, id, Eq, congrArg, propext, RestrictedProduct.continuous_rng_of_principal_iff_forall, continuous_pi_iff, Continuous.comp, RestrictedProduct.continuous_eval, continuous_apply
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def Homeomorph.restrictedProductPi The homeomorphism between a restricted product of finite products, and a finite product of restricted products, when the products are with respect to open subsets line 194 source
Source documentation
The homeomorphism between a restricted product of finite products, and a finite product of restricted products, when the products are with respect to open subsets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, TopologicalSpace, Set, IsOpen, Homeomorph, RestrictedProduct, Set.ofPred, Membership.mem, Filter.cofinite
Proof uses: Equiv, Equiv.restrictedProductPi, Homeomorph.mk
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def Homeomorph.restrictedProductPi {ι : Type*} {n : Type*} [Fintype n]
    {A : n → ι → Type*} [∀ j i, TopologicalSpace (A j i)]
    {C : (j : n) → (i : ι) → Set (A j i)} (hCopen : ∀ j i, IsOpen (C j i)) :
    Πʳ i, [Π j, A j i, {f | ∀ j, f j ∈ C j i}] ≃ₜ Π j, (Πʳ i, [A j i, C j i]) where
…
```
def ContinuousMulEquiv.restrictedProductPi line 214 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, TopologicalSpace, Group, Subgroup, IsOpen, ContinuousMulEquiv, RestrictedProduct, Subgroup.pi, Set.univ, Filter.cofinite
Proof uses: ContinuousMulEquiv.mk, MulEquiv.mk, Equiv.mk, RestrictedProduct.map, RestrictedProduct.mk
40 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma ContinuousMulEquiv.restrictedProductPi_apply line 241 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, TopologicalSpace, Group, Subgroup, IsOpen, RestrictedProduct, Subgroup.pi, Set.univ, Filter.cofinite, Eq, ContinuousMulEquiv, ContinuousMulEquiv.restrictedProductPi
Proof uses: rfl
42 instances, coercions and auxiliary constants left out.
lemma ContinuousMulEquiv.restrictedProductPi_symm_apply line 250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, TopologicalSpace, Group, Subgroup, IsOpen, RestrictedProduct, Filter.cofinite, Eq, Subgroup.pi, Set.univ, ContinuousMulEquiv, ContinuousMulEquiv.symm, ContinuousMulEquiv.restrictedProductPi
Proof uses: rfl
42 instances, coercions and auxiliary constants left out.
theorem Homeomorph.restrictedProductMatrix_aux line 258 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, TopologicalSpace, Set, IsOpen, Set.ofPred, Membership.mem
Proof uses: Eq.mpr, Set.pi, Set.univ, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, Set.ext, of_eq_true, Iff, Eq.trans, True, congrArg, forall_congr, implies_congr, iff_self, isOpen_set_pi, Set.toFinite
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def Homeomorph.restrictedProductMatrix The homeomorphism between a restricted product of m x n matrices, and m x n matrices of restricted products, when the products are with respect to open sets line 269 source
Source documentation
The homeomorphism between a restricted product of m x n matrices, and m x n matrices of restricted products, when the products are with respect to open sets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, TopologicalSpace, Set, IsOpen, Homeomorph, RestrictedProduct, Matrix, Set.matrix, Filter.cofinite
Proof uses: Homeomorph.trans, Set.ofPred, Membership.mem, Homeomorph.restrictedProductPi, Homeomorph.piCongrRight
7 instances, coercions and auxiliary constants left out.
```
def Homeomorph.restrictedProductMatrix {ι : Type*} {m n : Type*} [Fintype m] [Fintype n]
    {A : ι → Type*} [∀ i, TopologicalSpace (A i)]
    {C : (i : ι) → Set (A i)} (hCopen : ∀ i, IsOpen (C i)) :
    Πʳ i, [Matrix m n (A i), (C i).matrix] ≃ₜ Matrix m n (Πʳ i, [A i, C i]) :=
…
```
lemma Homeomorph.restrictedProductMatrix_apply line 277 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, TopologicalSpace, Set, IsOpen, RestrictedProduct, Matrix, Set.matrix, Filter.cofinite, Eq, Homeomorph, Homeomorph.restrictedProductMatrix
Proof uses: rfl
12 instances, coercions and auxiliary constants left out.
lemma Homeomorph.restrictedProductMatrix_symm_apply line 284 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, TopologicalSpace, Set, IsOpen, Matrix, RestrictedProduct, Filter.cofinite, Eq, Set.matrix, Homeomorph, Homeomorph.symm, Homeomorph.restrictedProductMatrix
Proof uses: rfl
12 instances, coercions and auxiliary constants left out.
lemma Homeomorph.restrictedProductMatrix_toEquiv line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, TopologicalSpace, Set, IsOpen, Eq, Equiv, RestrictedProduct, Matrix, Set.matrix, Filter.cofinite, Homeomorph.toEquiv, Homeomorph.restrictedProductMatrix, Equiv.restrictedProductMatrix
Proof uses: rfl
4 instances, coercions and auxiliary constants left out.
def Submonoid.unitsContinuousMulEquivUnitsType line 303 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Monoid, Submonoid, IsOpen, ContinuousMulEquiv, Subtype, Units, Membership.mem, Subgroup, Submonoid.units
Proof uses: MulEquiv, Submonoid.unitsEquivUnitsType, ContinuousMulEquiv.mk
24 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
def ContinuousMulEquiv.restrictedProductUnits Documented declaration: restrictedProductUnits line 331 source
Source documentation
The monoid homeomorphism between the units of a restricted product of topological monoids and the restricted product of the units of the monoids, when the products are with respect to open submonoids.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, TopologicalSpace, ContinuousMul, SetLike, SubmonoidClass, IsOpen, ContinuousMulEquiv, Units, RestrictedProduct, Filter.cofinite, Subgroup, Submonoid.units, Submonoid.ofClass
Proof uses: Fact, MonoidHom, Subtype, Membership.mem, Submonoid, RestrictedProduct.structureMapMonoidHom, Homeomorph, ContinuousMulEquiv.toHomeomorph, ContinuousMulEquiv.piUnits, Homeomorph.piCongrRight, ContinuousMulEquiv.symm, Submonoid.unitsContinuousMulEquivUnitsType, RestrictedProduct.structureMap, MulEquiv, MulEquiv.restrictedProductUnits, ContinuousMulEquiv.mk
46 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
def ContinuousMulEquiv.restrictedProductUnits {ι : Type*}
    {M : ι → Type*} [(i : ι) → Monoid (M i)] [(i : ι) → TopologicalSpace (M i)]
    [(i : ι) → ContinuousMul (M i)]
    {S : ι → Type*} [∀ i, SetLike (S i) (M i)] [∀ i, SubmonoidClass (S i) (M i)]
    (A : Π i, S i) (hA : ∀ i, IsOpen (A i : Set (M i))) :
    (Πʳ i, [M i, A i])ˣ ≃ₜ*
      Πʳ i, [(M i)ˣ, (Submonoid.ofClass (A i)).units] :=
…
```
lemma RestrictedProduct.coe_sum line 373 source
standard axioms: Quot.sound, propext what this means
Statement uses: SetLike, AddCommMonoid, AddSubmonoidClass, Filter, Finset, RestrictedProduct, Eq, Finset.sum
Proof uses: map_sum, AddMonoidHom, RestrictedProduct.coeAddMonoidHom
17 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.sum_apply line 379 source
standard axioms: Quot.sound, propext what this means
Statement uses: SetLike, AddCommMonoid, AddSubmonoidClass, Filter, Finset, RestrictedProduct, Eq, Finset.sum
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, congrFun, RestrictedProduct.coe_sum, Finset.sum_apply, eq_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def ContinuousMulEquiv.restrictedProductMatrix The monoid homeomorphism between a restricted product of n x n matrices, and n x n matrices of restricted products, when the products are with respect to open sets line 389 source
Source documentation
The monoid homeomorphism between a restricted product of n x n matrices, and n x n matrices of restricted products, when the products are with respect to open sets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, TopologicalSpace, Ring, Subring, IsOpen, ContinuousMulEquiv, RestrictedProduct, Matrix, Subring.matrix, Filter.cofinite
Proof uses: Homeomorph, Set.matrix, Homeomorph.restrictedProductMatrix, ContinuousMulEquiv.mk, MulEquiv.mk, Homeomorph.toEquiv
42 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def ContinuousMulEquiv.restrictedProductMatrix {ι : Type*}
    {n : Type*} [Fintype n] [DecidableEq n]
    {A : ι → Type*} [∀ i, TopologicalSpace (A i)] [∀ i, Ring (A i)]
    {C : (i : ι) → Subring (A i)} (hCopen : ∀ i, IsOpen ((C i) : Set (A i))) :
      Πʳ i, [Matrix n n (A i), ((C i).matrix : Subring (Matrix n n (A i)))]
      ≃ₜ* Matrix n n (Πʳ i, [A i, C i]) where
…
```
lemma ContinuousMulEquiv.restrictedProductMatrix_apply line 399 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, TopologicalSpace, Ring, Subring, IsOpen, RestrictedProduct, Matrix, Subring.matrix, Filter.cofinite, Eq, ContinuousMulEquiv, ContinuousMulEquiv.restrictedProductMatrix
Proof uses: rfl
54 instances, coercions and auxiliary constants left out.
lemma ContinuousMulEquiv.restrictedProductMatrix_symm_apply line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, TopologicalSpace, Ring, Subring, IsOpen, Matrix, RestrictedProduct, Filter.cofinite, Eq, Subring.matrix, ContinuousMulEquiv, ContinuousMulEquiv.symm, ContinuousMulEquiv.restrictedProductMatrix
Proof uses: rfl
54 instances, coercions and auxiliary constants left out.
def ContinuousMulEquiv.restrictedProductMatrixUnits Documented declaration: restrictedProductMatrixUnits line 419 source
Source documentation
The monoid homeomorphism between the matrix units over a restricted product and the restricted product of the matrix units over the factors, when the products are with respect to open submonoids.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, TopologicalSpace, Ring, IsTopologicalRing, Subring, IsOpen, ContinuousMulEquiv, Units, Matrix, RestrictedProduct, Filter.cofinite, Subgroup, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, Subring.matrix
Proof uses: ContinuousMulEquiv.trans, ContinuousMulEquiv.symm, ContinuousMulEquiv.mapUnits, ContinuousMulEquiv.restrictedProductMatrix, ContinuousMulEquiv.restrictedProductUnits
46 instances, coercions and auxiliary constants left out.
```
def ContinuousMulEquiv.restrictedProductMatrixUnits {ι : Type*}
    {n : Type*} [Fintype n] [DecidableEq n]
    {A : ι → Type*} [∀ i, TopologicalSpace (A i)] [∀ i, Ring (A i)] [∀ i, IsTopologicalRing (A i)]
    {C : (i : ι) → Subring (A i)} (hCopen : ∀ i, IsOpen ((C i) : Set (A i))) :
    (Matrix n n (Πʳ i, [A i, C i]))ˣ ≃ₜ*
      Πʳ i, [(Matrix n n (A i))ˣ, ((C i).matrix.units : Subgroup (Matrix n n (A i))ˣ)] :=
…
```
lemma ContinuousMulEquiv.restrictedProductMatrixUnits_apply line 429 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, TopologicalSpace, Ring, IsTopologicalRing, Subring, IsOpen, Units, Matrix, RestrictedProduct, Filter.cofinite, Eq, Subgroup, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, Subring.matrix, ContinuousMulEquiv, ContinuousMulEquiv.restrictedProductMatrixUnits
Proof uses: rfl
56 instances, coercions and auxiliary constants left out.
lemma ContinuousMulEquiv.restrictedProductMatrixUnits_symm_apply line 437 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, TopologicalSpace, Ring, IsTopologicalRing, Subring, IsOpen, RestrictedProduct, Units, Matrix, Subgroup, Submonoid.units, Subsemiring.toSubmonoid, Subring.toSubsemiring, Subring.matrix, Filter.cofinite, Eq, ContinuousMulEquiv, ContinuousMulEquiv.symm, ContinuousMulEquiv.restrictedProductMatrixUnits
Proof uses: rfl
56 instances, coercions and auxiliary constants left out.
def RestrictedProduct.flattenHomeomorph The canonical homeomorphism from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set line 457 source
Source documentation
The canonical homeomorphism from a restricted product of products over fibres of a map on indexing sets to the restricted product over the original indexing set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Eq, Filter.comap, TopologicalSpace, Homeomorph, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ
Proof uses: Equiv, RestrictedProduct.flattenEquiv, Homeomorph.mk
14 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
def flattenHomeomorph :
    Πʳ j, [Π (i : f ⁻¹' {j}), G i, Set.pi Set.univ (fun (i : f ⁻¹' {j}) => C i)]_[𝒢] ≃ₜ
    Πʳ i, [G i, C i]_[ℱ] where
…
```
lemma RestrictedProduct.flatten_homeomorph_apply line 492 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Eq, Filter.comap, TopologicalSpace, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ, Homeomorph, RestrictedProduct.flattenHomeomorph, Subtype.mk, rfl
20 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.flatten_homeomorph_symm_apply line 497 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Eq, Filter.comap, TopologicalSpace, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ, Homeomorph, Homeomorph.symm, RestrictedProduct.flattenHomeomorph
Proof uses: rfl
20 instances, coercions and auxiliary constants left out.
def RestrictedProduct.flattenHomeomorph' The homeomorphism given by flatten when both restricted products are over the cofinite filter and there's a topology on the factors line 505 source
Source documentation
The homeomorphism given by flatten when both restricted products are over the cofinite filter and there's a topology on the factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, Filter.Tendsto, Filter.cofinite, Homeomorph, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ
Proof uses: RestrictedProduct.flattenHomeomorph
7 instances, coercions and auxiliary constants left out.
```
def flattenHomeomorph' :
    Πʳ j, [Π (i : f ⁻¹' {j}), G i, Set.pi Set.univ (fun (i : f ⁻¹' {j}) => C i)] ≃ₜ
    Πʳ i, [G i, C i] :=
…
```
lemma RestrictedProduct.flatten_homeomorph'_apply line 512 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, Filter.Tendsto, Filter.cofinite, RestrictedProduct, Set.preimage, Singleton.singleton, Membership.mem, Set.pi, Set.univ, Eq, Homeomorph, RestrictedProduct.flattenHomeomorph', Subtype.mk, rfl
20 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.flatten_homeomorph'_symm_apply line 517 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, Filter.Tendsto, Filter.cofinite, RestrictedProduct, Set.preimage, Singleton.singleton, Eq, Membership.mem, Set.pi, Set.univ, Homeomorph, Homeomorph.symm, RestrictedProduct.flattenHomeomorph'
Proof uses: rfl
20 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.mem_nhds_iff_of_principal An explicit condition for a set to be in the neighborhood of x : Πʳ i, [G i, C i]_[𝓟 T] in terms of a product of neighbourhoods on the factors line 533 source
Source documentation
An explicit condition for a set to be in the neighborhood of x : Πʳ i, [G i, C i]_[𝓟 T] in terms of a product of neighbourhoods on the factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, RestrictedProduct, Filter.principal, Iff, Membership.mem, Filter, nhds, Exists, And, Set.Finite, LE.le, Set.preimage, Set.pi
Proof uses: Eq.mpr, Filter.comap, id, Eq, congrArg, Topology.IsInducing.nhds_eq_comap, Topology.IsEmbedding.toIsInducing, RestrictedProduct.isEmbedding_coe_of_principal, propext, Filter.mem_comap, Filter.pi, nhds_pi, congrFun', funext, Iff.intro, Exists.intro, And.intro, le_imp_le_of_le_of_le, Set.preimage_mono, le_refl and 1 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma RestrictedProduct.mem_nhds_iff_of_principal {T : Set ι} {x : Πʳ i, [G i, C i]_[𝓟 T]}
    (U : Set Πʳ i, [G i, C i]_[𝓟 T]) :
    U ∈ nhds x ↔ ∃ (I : Set ι) (s : (i : ι) → Set (G i)), I.Finite ∧ (∀ i, s i ∈ nhds (x i)) ∧
    (↑) ⁻¹' I.pi s ⊆ U := by
…
```
lemma RestrictedProduct.mem_nhds_of_exists_nhds_of_cofinite A condition for a set to be a neighborhood in Πʳ i, [G i, C i], slightly weaker than the condition in mem_nhds_iff_of_cofinite line 545 source
Source documentation
A condition for a set to be a neighborhood in Πʳ i, [G i, C i], slightly weaker than the condition in mem_nhds_iff_of_cofinite.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, RestrictedProduct, Filter.cofinite, IsOpen, Membership.mem, Filter, nhds, Filter.Eventually, LE.le, Set.preimage, Set.pi, Set.univ
Proof uses: Set.ofPred, Not, Eq, rfl, Filter.principal, Compl.compl, Eq.mpr, Set.Finite, id, Eq.trans, congrArg, compl_compl, Eq.mp, RestrictedProduct.eventually, of_eq_true, True, forall_congr, implies_congr, Eq.refl, implies_true and 34 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma RestrictedProduct.mem_nhds_of_exists_nhds_of_cofinite {x : Πʳ i, [G i, C i]}
    {U : Set Πʳ i, [G i, C i]} (hCopen : ∀ i, IsOpen (C i : Set (G i))) (s : (i : ι) → Set (G i))
    (hs : ∀ i, s i ∈ nhds (x i)) (hf : ∀ᶠ i in Filter.cofinite, C i ⊆ s i)
    (hU : (↑) ⁻¹' Set.univ.pi s ⊆ U) : U ∈ nhds x := by
…
```
lemma RestrictedProduct.mem_nhds_iff_of_cofinite The classical condition for a set to be a neighborhood in the restricted product line 569 source
Source documentation
The classical condition for a set to be a neighborhood in the restricted product.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, RestrictedProduct, Filter.cofinite, IsOpen, Iff, Membership.mem, Filter, nhds, Exists, And, Filter.Eventually, Eq, LE.le, Set.pi, Set.univ, Set.image
Proof uses: Iff.intro, Set.ofPred, Not, rfl, Filter.principal, Compl.compl, Eq.mpr, Set.Finite, id, Eq.trans, congrArg, compl_compl, Eq.mp, RestrictedProduct.eventually, of_eq_true, True, forall_congr, implies_congr, Eq.refl, implies_true and 51 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma RestrictedProduct.mem_nhds_iff_of_cofinite {x : Πʳ i, [G i, C i]} {U : Set Πʳ i, [G i, C i]}
    (hCopen : ∀ i, IsOpen (C i : Set (G i))) :
    U ∈ nhds x ↔ ∃ (s : (i : ι) → Set (G i)), (∀ i, s i ∈ nhds (x i)) ∧
    (∀ᶠ i in Filter.cofinite, s i = C i) ∧ Set.univ.pi s ⊆ (↑) '' U := by
…
```
lemma RestrictedProduct.isOpenMap_of_open_components line 602 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, IsOpen, RestrictedProduct, Filter.cofinite, Eq, IsOpenMap, Filter.Eventually, Set.SurjOn
Proof uses: IsOpenMap.of_nhds_le, Filter.le_map, nhds, Membership.mem, Filter, And, LE.le, Set.pi, Set.univ, Set.image, Exists, Iff.mp, RestrictedProduct.mem_nhds_iff_of_cofinite, RestrictedProduct.mem_nhds_of_exists_nhds_of_cofinite, Eq.mpr, id, congrArg, IsOpenMap.image_mem_nhds, Filter.mp_mem, Set.ofPred and 15 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
instance RestrictedProduct.SecondCountableTopology_of_principal line 623 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, TopologicalSpace, Set, SecondCountableTopology, RestrictedProduct, Filter.principal
Proof uses: Topology.IsEmbedding.secondCountableTopology, RestrictedProduct.isEmbedding_coe_of_principal
6 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.secondCountableTopology line 633 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, TopologicalSpace, Set, IsOpen, SecondCountableTopology, RestrictedProduct, Filter.cofinite
Proof uses: TopologicalSpace.secondCountableTopology_of_countable_cover', Filter.sets, Filter.principal, Membership.mem, RestrictedProduct.inclusion, Iff.mpr, LE.le, Filter, Filter.le_principal_iff, Subtype.property, RestrictedProduct.isOpenEmbedding_inclusion_principal, Exists.intro, Exists, Eq, Subtype.mk, Set.ofPred, Filter.Eventually, of_eq_true, Eq.trans, True and 6 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Homeomorph.restrictedProductPrincipal The canonical homeomorphism between a restricted product Πʳ i, [R i, A i]_[𝓟 J] over a principal filter, and the corresponding product (Π i : J, A i) × (Π i : Jᶜ, R i) line 651 source
Source documentation
The canonical homeomorphism between a restricted product Πʳ i, [R i, A i]_[𝓟 J] over a principal filter, and the corresponding product (Π i : J, A i) × (Π i : Jᶜ, R i).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, TopologicalSpace, Homeomorph, RestrictedProduct, Filter.principal, Prod, Membership.mem, Compl.compl
Proof uses: Equiv, RestrictedProduct.principalEquivProd, Classical.propDecidable, Homeomorph.mk
18 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
noncomputable def Homeomorph.restrictedProductPrincipal {ι : Type*}
    (R : ι → Type*) (A : Π i, Set (R i)) [∀ i, TopologicalSpace (R i)] (J : Set ι) :
    Πʳ i, [R i, A i]_[𝓟 J] ≃ₜ (Π i : J, A i) × (Π i : (Jᶜ : Set ι), R i) where
…
```
def ContinuousMulEquiv.restrictedProductPrincipal line 673 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monoid, TopologicalSpace, SetLike, SubmonoidClass, Set, ContinuousMulEquiv, RestrictedProduct, Filter.principal, Prod, Subtype, Membership.mem, Compl.compl
Proof uses: Homeomorph, Homeomorph.restrictedProductPrincipal, ContinuousMulEquiv.mk, MulEquiv.mk, Homeomorph.toEquiv
40 instances, coercions and auxiliary constants left out.
def RestrictedProduct.singleContinuousAddMonoidHom The inclusion from a factor into the restricted product of topological additive groups, as a continuous group homomorphism line 698 source
Source documentation
The inclusion from a factor into the restricted product of topological additive groups, as a continuous group homomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SetLike, AddCommMonoid, AddSubmonoidClass, TopologicalSpace, ContinuousAddMonoidHom, RestrictedProduct, Filter.cofinite
Proof uses: AddMonoidHom, RestrictedProduct.singleAddMonoidHom, ContinuousAddMonoidHom.mk
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
noncomputable def singleContinuousAddMonoidHom (j : ι) : A j →ₜ+ Πʳ i, [A i, B i] where
…
```
lemma RestrictedProduct.singleContinuousAddMonoidHom_apply_same line 711 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SetLike, AddCommMonoid, AddSubmonoidClass, TopologicalSpace, Eq, RestrictedProduct, Filter.cofinite, ContinuousAddMonoidHom, RestrictedProduct.singleContinuousAddMonoidHom
Proof uses: Pi.single_eq_same
12 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.singleContinuousAddMonoidHom_apply_of_ne line 715 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SetLike, AddCommMonoid, AddSubmonoidClass, TopologicalSpace, Ne, Eq, RestrictedProduct, Filter.cofinite, ContinuousAddMonoidHom, RestrictedProduct.singleContinuousAddMonoidHom, OfNat.ofNat
Proof uses: Pi.single_eq_of_ne
15 instances, coercions and auxiliary constants left out.
def RestrictedProduct.evalContinuousAddMonoidHom The continuous additive projection from a restricted product of topological additive groups to a factor line 732 source
Source documentation
The continuous additive projection from a restricted product of topological additive groups to a factor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, AddCommMonoid, AddSubmonoidClass, TopologicalSpace, ContinuousAddMonoidHom, RestrictedProduct, Filter.cofinite
Proof uses: AddMonoidHom, RestrictedProduct.evalAddMonoidHom, ContinuousAddMonoidHom.mk
12 instances, coercions and auxiliary constants left out.
```
def evalContinuousAddMonoidHom (j : ι) : Πʳ i, [A i, B i] →ₜ+ A j := {
…
```