Description of locally finite families from a nonstandard point of view

ULF LEONARD CLOTZ

studies the neighbourhood-monads of the standard points. Here we look at neighborhood filter in Lean and prove uniqueness of limits.