MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-bn Unicode version

Definition df-bn 18758
Description: Define the class of all Banach spaces. A Banach space is a normed vector space such that both the vector space and the scalar field are complete under their respective norm-induced metrics. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
Assertion
Ref Expression
df-bn  |- Ban  =  {
w  e.  (NrmVec  i^i CMetSp )  |  (Scalar `  w
)  e. CMetSp }

Detailed syntax breakdown of Definition df-bn
StepHypRef Expression
1 cbn 18755 . 2  class Ban
2 vw . . . . . 6  set  w
32cv 1622 . . . . 5  class  w
4 csca 13211 . . . . 5  class Scalar
53, 4cfv 5255 . . . 4  class  (Scalar `  w )
6 ccms 18754 . . . 4  class CMetSp
75, 6wcel 1684 . . 3  wff  (Scalar `  w )  e. CMetSp
8 cnvc 18104 . . . 4  class NrmVec
98, 6cin 3151 . . 3  class  (NrmVec  i^i CMetSp )
107, 2, 9crab 2547 . 2  class  { w  e.  (NrmVec  i^i CMetSp )  |  (Scalar `  w )  e. CMetSp }
111, 10wceq 1623 1  wff Ban  =  {
w  e.  (NrmVec  i^i CMetSp )  |  (Scalar `  w
)  e. CMetSp }
Colors of variables: wff set class
This definition is referenced by:  isbn  18760
  Copyright terms: Public domain W3C validator