def AbstractHeckeOperator.HeckeOperator_toFun.{u_1,
    u_2}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_1] {AType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u} (M : Type u) : Type uAn additive commutative monoid is an additive monoid with commutative `(+)`.  AType u_2] [DistribMulActionDistribMulAction.{u_12, u_13} (M : Type u_12) (A : Type u_13) [Monoid M] [AddMonoid A] : Type (max u_12 u_13)Typeclass for multiplicative actions on additive structures.

For example, if `G` is a group (with group law written as multiplication) and `A` is an
abelian group (with group law written as addition), then to give `A` a `G`-module
structure (for example, to use the theory of group cohomology) is to say `[DistribMulAction G A]`.
Note in that we do not use the `Module` typeclass for `G`-modules, as the `Module` typeclass
is for modules over a ring rather than a group.

Mathematically, `DistribMulAction G A` is equivalent to giving `A` the structure of
a `ℤ[G]`-module.
 GType u_1 AType u_2]
  {gG : GType u_1} {USubgroup G VSubgroup G : SubgroupSubgroup.{u_3} (G : Type u_3) [Group G] : Type u_3A subgroup of a group `G` is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.  GType u_1}
  (h(QuotientGroup.mk '' (↑U * {g})).Finite :
    (Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. QuotientGroup.mkQuotientGroup.mk.{u_1} {α : Type u_1} [Group α] {s : Subgroup α} (a : α) : α ⧸ sThe canonical map from a group `α` to the quotient `α ⧸ s`.  ''Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. 
        (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.↑USubgroup G *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. {Singleton.singleton.{u, v} {α : outParam (Type u)} {β : Type v} [self : Singleton α β] : α → β`singleton x` is a collection with the single element `x` (notation: `{x}`). 

Conventions for notations in identifiers:

 * The recommended spelling of `{x}` in identifiers is `singleton`.gG}Singleton.singleton.{u, v} {α : outParam (Type u)} {β : Type v} [self : Singleton α β] : α → β`singleton x` is a collection with the single element `x` (notation: `{x}`). 

Conventions for notations in identifiers:

 * The recommended spelling of `{x}` in identifiers is `singleton`.)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.)Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. .FiniteSet.Finite.{u} {α : Type u} (s : Set α) : PropA set is finite if the corresponding `Subtype` is finite,
i.e., if there exists a natural `n : ℕ` and an equivalence `s ≃ Fin n`. )
  (a↑(MulAction.fixedPoints (↥V) A) : ↑(MulAction.fixedPointsMulAction.fixedPoints.{u_1, u_3} (M : Type u_1) (α : Type u_3) [Monoid M] [MulAction M α] : Set αThe set of elements fixed under the whole action.  (↥VSubgroup G) AType u_2)) :
  ↑(MulAction.fixedPointsMulAction.fixedPoints.{u_1, u_3} (M : Type u_1) (α : Type u_3) [Monoid M] [MulAction M α] : Set αThe set of elements fixed under the whole action.  (↥USubgroup G) AType u_2)

def AbstractHeckeOperator.HeckeOperator.{u_1,
    u_2, u_3}
  {GType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [GroupGroup.{u} (G : Type u) : Type uA `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
 GType u_1] {AType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommMonoidAddCommMonoid.{u} (M : Type u) : Type uAn additive commutative monoid is an additive monoid with commutative `(+)`.  AType u_2] [DistribMulActionDistribMulAction.{u_12, u_13} (M : Type u_12) (A : Type u_13) [Monoid M] [AddMonoid A] : Type (max u_12 u_13)Typeclass for multiplicative actions on additive structures.

For example, if `G` is a group (with group law written as multiplication) and `A` is an
abelian group (with group law written as addition), then to give `A` a `G`-module
structure (for example, to use the theory of group cohomology) is to say `[DistribMulAction G A]`.
Note in that we do not use the `Module` typeclass for `G`-modules, as the `Module` typeclass
is for modules over a ring rather than a group.

Mathematically, `DistribMulAction G A` is equivalent to giving `A` the structure of
a `ℤ[G]`-module.
 GType u_1 AType u_2]
  (gG : GType u_1) (USubgroup G VSubgroup G : SubgroupSubgroup.{u_3} (G : Type u_3) [Group G] : Type u_3A subgroup of a group `G` is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.  GType u_1)
  (h(QuotientGroup.mk '' (↑U * {g})).Finite :
    (Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. QuotientGroup.mkQuotientGroup.mk.{u_1} {α : Type u_1} [Group α] {s : Subgroup α} (a : α) : α ⧸ sThe canonical map from a group `α` to the quotient `α ⧸ s`.  ''Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. 
        (HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.↑USubgroup G *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. {Singleton.singleton.{u, v} {α : outParam (Type u)} {β : Type v} [self : Singleton α β] : α → β`singleton x` is a collection with the single element `x` (notation: `{x}`). 

Conventions for notations in identifiers:

 * The recommended spelling of `{x}` in identifiers is `singleton`.gG}Singleton.singleton.{u, v} {α : outParam (Type u)} {β : Type v} [self : Singleton α β] : α → β`singleton x` is a collection with the single element `x` (notation: `{x}`). 

Conventions for notations in identifiers:

 * The recommended spelling of `{x}` in identifiers is `singleton`.)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.)Set.image.{u, v} {α : Type u} {β : Type v} (f : α → β) (s : Set α) : Set βThe image of `s : Set α` by `f : α → β`, written `f '' s`, is the set of `b : β` such that
`f a = b` for some `a ∈ s`. .FiniteSet.Finite.{u} {α : Type u} (s : Set α) : PropA set is finite if the corresponding `Subtype` is finite,
i.e., if there exists a natural `n : ℕ` and an equivalence `s ≃ Fin n`. )
  {RType u_3 : Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [RingRing.{u} (R : Type u) : Type uA `Ring` is a `Semiring` with negation making it an additive group.  RType u_3] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  RType u_3 AType u_2]
  [SMulCommClassSMulCommClass.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M α] [SMul N α] : PropA typeclass mixin saying that two multiplicative actions on the same space commute.  GType u_1 RType u_3 AType u_2] :
  ↑(MulAction.fixedPointsMulAction.fixedPoints.{u_1, u_3} (M : Type u_1) (α : Type u_3) [Monoid M] [MulAction M α] : Set αThe set of elements fixed under the whole action.  (↥VSubgroup G) AType u_2) →ₗ[LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  Type (max u_16 u_17)A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. RType u_3]LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  Type (max u_16 u_17)A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. 
    ↑(MulAction.fixedPointsMulAction.fixedPoints.{u_1, u_3} (M : Type u_1) (α : Type u_3) [Monoid M] [MulAction M α] : Set αThe set of elements fixed under the whole action.  (↥USubgroup G) AType u_2)

def Homeomorph.restrictedProductProd.{u_4,
    u_5, u_6}
  {ιType u_4 : Type u_4A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {Aι → Type u_5 : ιType u_4 → Type u_5A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {Bι → Type u_6 : ιType u_4 → Type u_6A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {C(i : ι) → Set (A i) : (iι : ιType u_4) → SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 (Aι → Type u_5 iι)}
  {D(i : ι) → Set (B i) : (iι : ιType u_4) → SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 (Bι → Type u_6 iι)}
  [(iι : ιType u_4) → TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  (Aι → Type u_5 iι)]
  [(iι : ιType u_4) → TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  (Bι → Type u_6 iι)]
  (hCopen∀ (i : ι), IsOpen (C i) : ∀ (iι : ιType u_4), IsOpenIsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop`IsOpen s` means that `s` is open in the ambient topological space on `X`  (C(i : ι) → Set (A i) iι))
  (hDopen∀ (i : ι), IsOpen (D i) : ∀ (iι : ιType u_4), IsOpenIsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop`IsOpen s` means that `s` is open in the ambient topological space on `X`  (D(i : ι) → Set (B i) iι)) :
  RestrictedProductRestrictedProduct.{u_1, u_2} {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) :
  Type (max u_1 u_2)The **restricted product** of a family `R : ι → Type*` of types, relative to subsets
`A : (i : ι) → Set (R i)` and the filter `𝓕 : Filter ι`, is the set of all `x : Π i, R i`
such that the set `{j | x j ∈ A j}` belongs to `𝓕`. We denote it by `Πʳ i, [R i, A i]_[𝓕]`.

The most common use case is with `𝓕 = cofinite`, in which case the restricted product is the set
of all `x : Π i, R i` such that `x j ∈ A j` for all but finitely many `j`. We denote it simply
by `Πʳ i, [R i, A i]`.

Similarly, if `S` is a principal filter, the restricted product `Πʳ i, [R i, A i]_[𝓟 s]`
is the set of all `x : Π i, R i` such that `∀ j ∈ S, x j ∈ A j`.  (fun iι ↦ Aι → Type u_5 iι ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. Bι → Type u_6 iι)
      (fun iι ↦ C(i : ι) → Set (A i) iι ×ˢSProd.sprod.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : SProd α β γ] : α → β → γThe Cartesian product `s ×ˢ t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`.  D(i : ι) → Set (B i) iι)
      Filter.cofiniteFilter.cofinite.{u_2} {α : Type u_2} : Filter αThe cofinite filter is the filter of subsets whose complements are finite.  ≃ₜHomeomorph.{u_5, u_6} (X : Type u_5) (Y : Type u_6) [TopologicalSpace X] [TopologicalSpace Y] : Type (max u_5 u_6)Homeomorphism between `X` and `Y`, also called topological isomorphism 
    RestrictedProductRestrictedProduct.{u_1, u_2} {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) :
  Type (max u_1 u_2)The **restricted product** of a family `R : ι → Type*` of types, relative to subsets
`A : (i : ι) → Set (R i)` and the filter `𝓕 : Filter ι`, is the set of all `x : Π i, R i`
such that the set `{j | x j ∈ A j}` belongs to `𝓕`. We denote it by `Πʳ i, [R i, A i]_[𝓕]`.

The most common use case is with `𝓕 = cofinite`, in which case the restricted product is the set
of all `x : Π i, R i` such that `x j ∈ A j` for all but finitely many `j`. We denote it simply
by `Πʳ i, [R i, A i]`.

Similarly, if `S` is a principal filter, the restricted product `Πʳ i, [R i, A i]_[𝓟 s]`
is the set of all `x : Π i, R i` such that `∀ j ∈ S, x j ∈ A j`.  (fun iι ↦ Aι → Type u_5 iι)
        (fun iι ↦ C(i : ι) → Set (A i) iι) Filter.cofiniteFilter.cofinite.{u_2} {α : Type u_2} : Filter αThe cofinite filter is the filter of subsets whose complements are finite.  ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.
      RestrictedProductRestrictedProduct.{u_1, u_2} {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) :
  Type (max u_1 u_2)The **restricted product** of a family `R : ι → Type*` of types, relative to subsets
`A : (i : ι) → Set (R i)` and the filter `𝓕 : Filter ι`, is the set of all `x : Π i, R i`
such that the set `{j | x j ∈ A j}` belongs to `𝓕`. We denote it by `Πʳ i, [R i, A i]_[𝓕]`.

The most common use case is with `𝓕 = cofinite`, in which case the restricted product is the set
of all `x : Π i, R i` such that `x j ∈ A j` for all but finitely many `j`. We denote it simply
by `Πʳ i, [R i, A i]`.

Similarly, if `S` is a principal filter, the restricted product `Πʳ i, [R i, A i]_[𝓟 s]`
is the set of all `x : Π i, R i` such that `∀ j ∈ S, x j ∈ A j`.  (fun iι ↦ Bι → Type u_6 iι)
        (fun iι ↦ D(i : ι) → Set (B i) iι) Filter.cofiniteFilter.cofinite.{u_2} {α : Type u_2} : Filter αThe cofinite filter is the filter of subsets whose complements are finite. 

def Homeomorph.restrictedProductPi.{u_7, u_8,
    u_9}
  {ιType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {nType u_8 : Type u_8A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  nType u_8] {An → ι → Type u_9 : nType u_8 → ιType u_7 → Type u_9A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [(jn : nType u_8) →
      (iι : ιType u_7) → TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  (An → ι → Type u_9 jn iι)]
  {C(j : n) → (i : ι) → Set (A j i) : (jn : nType u_8) → (iι : ιType u_7) → SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 (An → ι → Type u_9 jn iι)}
  (hCopen∀ (j : n) (i : ι), IsOpen (C j i) :
    ∀ (jn : nType u_8) (iι : ιType u_7), IsOpenIsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop`IsOpen s` means that `s` is open in the ambient topological space on `X`  (C(j : n) → (i : ι) → Set (A j i) jn iι)) :
  RestrictedProductRestrictedProduct.{u_1, u_2} {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) :
  Type (max u_1 u_2)The **restricted product** of a family `R : ι → Type*` of types, relative to subsets
`A : (i : ι) → Set (R i)` and the filter `𝓕 : Filter ι`, is the set of all `x : Π i, R i`
such that the set `{j | x j ∈ A j}` belongs to `𝓕`. We denote it by `Πʳ i, [R i, A i]_[𝓕]`.

The most common use case is with `𝓕 = cofinite`, in which case the restricted product is the set
of all `x : Π i, R i` such that `x j ∈ A j` for all but finitely many `j`. We denote it simply
by `Πʳ i, [R i, A i]`.

Similarly, if `S` is a principal filter, the restricted product `Πʳ i, [R i, A i]_[𝓟 s]`
is the set of all `x : Π i, R i` such that `∀ j ∈ S, x j ∈ A j`. 
      (fun iι ↦ (jn : nType u_8) → An → ι → Type u_9 jn iι)
      (fun iι ↦
        {setOf.{u} {α : Type u} (p : α → Prop) : Set αTurn a predicate `p : α → Prop` into a set, also written as `{x | p x}` f(fun i ↦ (j : n) → A j i) i |setOf.{u} {α : Type u} (p : α → Prop) : Set αTurn a predicate `p : α → Prop` into a set, also written as `{x | p x}`  ∀ (jn : nType u_8), f(fun i ↦ (j : n) → A j i) i jn ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. C(j : n) → (i : ι) → Set (A j i) jn iι}setOf.{u} {α : Type u} (p : α → Prop) : Set αTurn a predicate `p : α → Prop` into a set, also written as `{x | p x}` )
      Filter.cofiniteFilter.cofinite.{u_2} {α : Type u_2} : Filter αThe cofinite filter is the filter of subsets whose complements are finite.  ≃ₜHomeomorph.{u_5, u_6} (X : Type u_5) (Y : Type u_6) [TopologicalSpace X] [TopologicalSpace Y] : Type (max u_5 u_6)Homeomorphism between `X` and `Y`, also called topological isomorphism 
    ((jn : nType u_8) →
      RestrictedProductRestrictedProduct.{u_1, u_2} {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) :
  Type (max u_1 u_2)The **restricted product** of a family `R : ι → Type*` of types, relative to subsets
`A : (i : ι) → Set (R i)` and the filter `𝓕 : Filter ι`, is the set of all `x : Π i, R i`
such that the set `{j | x j ∈ A j}` belongs to `𝓕`. We denote it by `Πʳ i, [R i, A i]_[𝓕]`.

The most common use case is with `𝓕 = cofinite`, in which case the restricted product is the set
of all `x : Π i, R i` such that `x j ∈ A j` for all but finitely many `j`. We denote it simply
by `Πʳ i, [R i, A i]`.

Similarly, if `S` is a principal filter, the restricted product `Πʳ i, [R i, A i]_[𝓟 s]`
is the set of all `x : Π i, R i` such that `∀ j ∈ S, x j ∈ A j`.  (fun iι ↦ An → ι → Type u_9 jn iι)
        (fun iι ↦ C(j : n) → (i : ι) → Set (A j i) jn iι) Filter.cofiniteFilter.cofinite.{u_2} {α : Type u_2} : Filter αThe cofinite filter is the filter of subsets whose complements are finite. )

def Homeomorph.restrictedProductMatrix.{u_7,
    u_8, u_9, u_10}
  {ιType u_7 : Type u_7A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {mType u_8 : Type u_8A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  {nType u_9 : Type u_9A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  mType u_8] [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  nType u_9]
  {Aι → Type u_10 : ιType u_7 → Type u_10A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [(iι : ιType u_7) → TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  (Aι → Type u_10 iι)]
  {C(i : ι) → Set (A i) : (iι : ιType u_7) → SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 (Aι → Type u_10 iι)}
  (hCopen∀ (i : ι), IsOpen (C i) : ∀ (iι : ιType u_7), IsOpenIsOpen.{u} {X : Type u} [TopologicalSpace X] : Set X → Prop`IsOpen s` means that `s` is open in the ambient topological space on `X`  (C(i : ι) → Set (A i) iι)) :
  RestrictedProductRestrictedProduct.{u_1, u_2} {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) :
  Type (max u_1 u_2)The **restricted product** of a family `R : ι → Type*` of types, relative to subsets
`A : (i : ι) → Set (R i)` and the filter `𝓕 : Filter ι`, is the set of all `x : Π i, R i`
such that the set `{j | x j ∈ A j}` belongs to `𝓕`. We denote it by `Πʳ i, [R i, A i]_[𝓕]`.

The most common use case is with `𝓕 = cofinite`, in which case the restricted product is the set
of all `x : Π i, R i` such that `x j ∈ A j` for all but finitely many `j`. We denote it simply
by `Πʳ i, [R i, A i]`.

Similarly, if `S` is a principal filter, the restricted product `Πʳ i, [R i, A i]_[𝓟 s]`
is the set of all `x : Π i, R i` such that `∀ j ∈ S, x j ∈ A j`. 
      (fun iι ↦ MatrixMatrix.{u, u', v} (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)`Matrix m n R` is the type of matrices with entries in `R`, whose rows are indexed by `m`
and whose columns are indexed by `n`.  mType u_8 nType u_9 (Aι → Type u_10 iι))
      (fun iι ↦ (C(i : ι) → Set (A i) iι).matrixSet.matrix.{v, u_2, u_3} {m : Type u_2} {n : Type u_3} {α : Type v} (S : Set α) : Set (Matrix m n α)Given a set `S`, `S.matrix` is the set of matrices `M`
all of whose entries `M i j` belong to `S`. )
      Filter.cofiniteFilter.cofinite.{u_2} {α : Type u_2} : Filter αThe cofinite filter is the filter of subsets whose complements are finite.  ≃ₜHomeomorph.{u_5, u_6} (X : Type u_5) (Y : Type u_6) [TopologicalSpace X] [TopologicalSpace Y] : Type (max u_5 u_6)Homeomorphism between `X` and `Y`, also called topological isomorphism 
    MatrixMatrix.{u, u', v} (m : Type u) (n : Type u') (α : Type v) : Type (max u u' v)`Matrix m n R` is the type of matrices with entries in `R`, whose rows are indexed by `m`
and whose columns are indexed by `n`.  mType u_8 nType u_9
      (RestrictedProductRestrictedProduct.{u_1, u_2} {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) :
  Type (max u_1 u_2)The **restricted product** of a family `R : ι → Type*` of types, relative to subsets
`A : (i : ι) → Set (R i)` and the filter `𝓕 : Filter ι`, is the set of all `x : Π i, R i`
such that the set `{j | x j ∈ A j}` belongs to `𝓕`. We denote it by `Πʳ i, [R i, A i]_[𝓕]`.

The most common use case is with `𝓕 = cofinite`, in which case the restricted product is the set
of all `x : Π i, R i` such that `x j ∈ A j` for all but finitely many `j`. We denote it simply
by `Πʳ i, [R i, A i]`.

Similarly, if `S` is a principal filter, the restricted product `Πʳ i, [R i, A i]_[𝓟 s]`
is the set of all `x : Π i, R i` such that `∀ j ∈ S, x j ∈ A j`.  (fun iι ↦ Aι → Type u_10 iι)
        (fun iι ↦ C(i : ι) → Set (A i) iι) Filter.cofiniteFilter.cofinite.{u_2} {α : Type u_2} : Filter αThe cofinite filter is the filter of subsets whose complements are finite. )

def ContinuousMulEquiv.piUnits.{u_1, u_2}
  {ιType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {Mι → Type u_2 : ιType u_1 → Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [(iι : ιType u_1) → MonoidMonoid.{u} (M : Type u) : Type uA `Monoid` is a `Semigroup` with an element `1` such that `1 * a = a * 1 = a`.  (Mι → Type u_2 iι)]
  [(iι : ιType u_1) → TopologicalSpaceTopologicalSpace.{u} (X : Type u) : Type uA topology on `X`.  (Mι → Type u_2 iι)] :
  ((iι : ιType u_1) → Mι → Type u_2 iι)ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`.  ≃ₜ*ContinuousMulEquiv.{u, v} (G : Type u) [TopologicalSpace G] (H : Type v) [TopologicalSpace H] [Mul G] [Mul H] :
  Type (max u v)The structure of two-sided continuous isomorphisms between groups.
Note that both the map and its inverse have to be continuous.  ((iι : ιType u_1) → (Mι → Type u_2 iι)ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. )