OAI/Topology/CoarseAssembly/SeparableEmbedding.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Placing each separable cycle on the fixed ample coefficient space

  1. theorem OAI.CoarseAssembly.Analytic.orthonormal_countable line 14
  2. theorem OAI.CoarseAssembly.Analytic.exists_ampleIsometry line 35

    Source documentation

    Only an isometric embedding is needed; the orthogonal complement is handled by the identity extension of the Fredholm operator.

    theorem exists_ampleIsometry (H : HilbertSpace) :
    Nonempty (H →ₗᵢ[ℂ] lp (fun _ : ℕ => ℂ) 2) := by
…

    Mentions: OAI.CoarseAssembly.Analytic.HilbertSpace