Theorems · Theorem · functional analysis

ContinuousLinearEquiv.piUnique_symm_apply

∀ {α : Type u_9} [inst : Unique α] (R : Type u_10) [inst_1 : Semiring R] (f : α → Type u_11)
  [inst_2 : (x : α) → AddCommMonoid (f x)] [inst_3 : (x : α) → Module R (f x)]
  [inst_4 : (x : α) → TopologicalSpace (f x)], ⇑(ContinuousLinearEquiv.piUnique R f).symm = uniqueElim

Defined in

Mathlib.Topology.Algebra.Module.Equiv

Cited by

0 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniqueSemiringAddCommMonoidModuleTopologicalSpace