OAI/Analysis/OperatorAlgebra/IsometricCornerNorm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Operator norm transfer through an isometric inclusion.

  1. lemma OAI.WeakPureInfiniteness.isometricCornerLift_norm line 13
  2. lemma OAI.WeakPureInfiniteness.eq_isometricCornerLift_of_intertwines line 18
  3. lemma OAI.WeakPureInfiniteness.norm_eq_of_corner_intertwines line 32