HomeIsabelle/Phabricator

Added a couple of lemmas to shorten proofs for convergence in types of class…

Description

Added a couple of lemmas to shorten proofs for convergence in types of class real_normed_vector.

Details