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

Committed
Jonathan Julian Huerta y Munive <jonjulian23@gmail.com>Feb 3 2020, 1:23 PM
Parents
rAFPe0ffeae3b9c3: Fix inaccurate word choice.
Branches
Unknown
Tags
Unknown

Event Timeline