OAI/Analysis/PureInfiniteness/OneStepPointNormClosure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual point-norm topology on maps, and the closure step in KR02 7.20.

  1. lemma OAI.WeakPureInfiniteness.finite_approximation_of_mem_closure line 15
  2. lemma OAI.WeakPureInfiniteness.approximatelyOneStepAlong_of_mem_closure line 26