OAI/Analysis/Commutator/BoundedSequenceClosed.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.HilbertSequence.mapPre line 24
2. def OAI.Kadison.HilbertSequence.mapVector line 27
3. lemma OAI.Kadison.HilbertSequence.seq_sub' line 30
4. lemma OAI.Kadison.HilbertSequence.norm_map_difference_tendsto line 32
5. theorem OAI.Kadison.HilbertSequence.bounded_image_isClosed line 38