Metamath Proof Explorer
Table of Contents - 12.4.3. Metric space balls
- blfvalps
- blfval
- blvalps
- blval
- elblps
- elbl
- elbl2ps
- elbl2
- elbl3ps
- elbl3
- blcomps
- blcom
- xblpnfps
- xblpnf
- blpnf
- bldisj
- blgt0
- bl2in
- xblss2ps
- xblss2
- blss2ps
- blss2
- blhalf
- blfps
- blf
- blrnps
- blrn
- xblcntrps
- xblcntr
- blcntrps
- blcntr
- xbln0
- bln0
- blelrnps
- blelrn
- blssm
- unirnblps
- unirnbl
- blin
- ssblps
- ssbl
- blssps
- blss
- blssexps
- blssex
- ssblex
- blin2
- blbas
- blres
- xmeterval
- xmeter
- xmetec
- blssec
- blpnfctr
- xmetresbl