OAI/Analysis/WeakInfiniteness/CStarClosedRange.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.starHom_continuous line 13
2. def OAI.WeakPureInfiniteness.clipScale line 22
3. lemma OAI.WeakPureInfiniteness.clipScale_den_pos line 24
4. lemma OAI.WeakPureInfiniteness.continuous_clipScale line 28
5. lemma OAI.WeakPureInfiniteness.clipScale_eq_one line 33
6. lemma OAI.WeakPureInfiniteness.clipScale_bound line 37
7. theorem OAI.WeakPureInfiniteness.starHom_exists_lift_norm_le line 53
8. theorem OAI.WeakPureInfiniteness.starHom_isClosed_range line 94