Talk:Locally Compact iff Open Neighborhood contains Compact Set

This is pretty much the (current) definition of locally compact. I wonder if Mizar uses another (equivalent) definition. --barto (talk) 13:16, 9 September 2017 (EDT)