Theorems · Theorem · functional analysis

ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F],
  Topology.IsEmbedding ContinuousAlternatingMap.toContinuousMultilinearMap

Defined in: Mathlib.Topology.Algebra.Module.Alternating.Topology
Cited by: 3 results in Mathlib
Foundations: Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedField AddCommGroup Module TopologicalSpace AddCommGroup Module TopologicalSpace IsTopologicalAddGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
Modulestatement and proof · cited by 20,661
AddCommGroupstatement and proof · cited by 12,871
IsTopologicalAddGroupstatement and proof · cited by 1,394
NormedFieldstatement and proof · cited by 1,084
ContinuousMultilinearMapstatement · cited by 1,016
Topology.IsEmbeddingstatement · cited by 294
ContinuousAlternatingMapstatement · cited by 292
ContinuousAlternatingMap.toContinuousMultilinearMapstatement · cited by 72
IsUniformEmbedding.isEmbeddingproof · cited by 25
ContinuousAlternatingMap.isUniformEmbedding_toContinuousMultilinearMapproof · cited by 6

Cited by3

Results whose statement or proof uses this declaration.

ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iffproof · cited by 1
ContinuousAlternatingMap.continuous_toContinuousMultilinearMapproof · cited by 0
ContinuousAlternatingMap.isClosedEmbedding_toContinuousMultilinearMapproof · cited by 0