def ContinuousAddEquiv.toIntContinuousLinearEquiv {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [TopologicalSpace M] [AddCommGroup M₂] [TopologicalSpace M₂] (e : M ≃ₜ+ M₂) : M ≃L[ℤ] M₂

Equations

• e.toIntContinuousLinearEquiv = { toLinearEquiv := e.toIntLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.quotientPi {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → AddCommGroup (G i)] [(i : ι) → TopologicalSpace (G i)] [∀ (i : ι), IsTopologicalAddGroup (G i)] [Fintype ι] (p : (i : ι) → AddSubgroup (G i)) [DecidableEq ι] : ((i : ι) → G i) ⧸ AddSubgroup.pi Set.univ p ≃ₜ+ ((i : ι) → G i ⧸ p i)

Equations

• ContinuousAddEquiv.quotientPi p = (Submodule.quotientPiContinuousLinearEquiv fun (i : ι) => AddSubgroup.toIntSubmodule (p i)).toContinuousAddEquiv

def ContinuousMulEquiv.piUnique {ι : Type u_1} (M : ι → Type u_2) [(j : ι) → Mul (M j)] [(j : ι) → TopologicalSpace (M j)] [Unique ι] : ((j : ι) → M j) ≃ₜ* M default

A family indexed by a type with a unique element is ContinuousMulEquiv to the element at the single index.

Equations

• ContinuousMulEquiv.piUnique M = { toMulEquiv := MulEquiv.piUnique M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.piUnique {ι : Type u_1} (M : ι → Type u_2) [(j : ι) → Add (M j)] [(j : ι) → TopologicalSpace (M j)] [Unique ι] : ((j : ι) → M j) ≃ₜ+ M default

A family indexed by a type with a unique element is ContinuousAddEquiv to the element at the single index.

Equations

• ContinuousAddEquiv.piUnique M = { toAddEquiv := AddEquiv.piUnique M, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousMulEquiv.piEquivPiSubtypeProd {ι : Type u_1} (p : ι → Prop) (Y : ι → Type u_2) [(i : ι) → TopologicalSpace (Y i)] [(i : ι) → Mul (Y i)] [DecidablePred p] : ((i : ι) → Y i) ≃ₜ* ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)

Splits the indices of ∀ (i : ι), Y i along the predicate p. This is Equiv.piEquivPiSubtypeProd as a ContinuousMulEquiv.

Equations

• ContinuousMulEquiv.piEquivPiSubtypeProd p Y = { toEquiv := (Homeomorph.piEquivPiSubtypeProd p Y).toEquiv, map_mul' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def ContinuousAddEquiv.piEquivPiSubtypeProd {ι : Type u_1} (p : ι → Prop) (Y : ι → Type u_2) [(i : ι) → TopologicalSpace (Y i)] [(i : ι) → Add (Y i)] [DecidablePred p] : ((i : ι) → Y i) ≃ₜ+ ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)

Splits the indices of ∀ (i : ι), Y i along the predicate p. This is Equiv.piEquivPiSubtypeProd as a ContinuousAddEquiv.

Equations

• ContinuousAddEquiv.piEquivPiSubtypeProd p Y = { toEquiv := (Homeomorph.piEquivPiSubtypeProd p Y).toEquiv, map_add' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }