OAI/Analysis/KadisonKastler/UnitBallClosure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Unit balls in norm closures of complex linear subspaces

Radial contraction keeps approximants in their original subspace. It proves the norm-density statement needed for the separable test algebras.

  1. def OAI.KadisonKastler.unitBallClip line 18
  2. theorem OAI.KadisonKastler.unitBallClip_norm_le line 20
  3. theorem OAI.KadisonKastler.unitBallClip_eq_self line 26
  4. theorem OAI.KadisonKastler.continuous_unitBallClip line 29
  5. theorem OAI.KadisonKastler.unitBallClip_mem line 36
  6. theorem OAI.KadisonKastler.closure_submodule_unitBall line 41

    Source documentation

    The unit ball of a linear subspace is norm dense in the unit ball of its closure, even when the subspace is not closed.

    theorem closure_submodule_unitBall (S : Submodule ℂ B) :
    closure {x : B | x ∈ S ∧ ‖x‖ ≤ 1} =
      {x : B | x ∈ closure (S : Set B) ∧ ‖x‖ ≤ 1} := by
…