:: deftheorem defines InvertibleOperators LOPBAN13:def 3 :
for X, Y being non trivial RealBanachSpace holds InvertibleOperators (X,Y) = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } ;