OAI/Analysis/WeakInfiniteness/IntertwiningLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.starHomLimitFun line 28
2. lemma OAI.WeakPureInfiniteness.starHomLimitFun_tendsto line 31
3. def OAI.WeakPureInfiniteness.starHomLimit line 35
4. lemma OAI.WeakPureInfiniteness.starHomLimit_isometry line 53
5. lemma OAI.WeakPureInfiniteness.cauchySeq_isometries_of_dense line 64
6. def OAI.WeakPureInfiniteness.starEquivOfConvergentIsometries line 77