Update L02.lean#103

thomas-strohmann wants to merge 2 commits intoAlexKontorovich:mainAlexKontorovich/RealAnalysisGame:mainfrom

thomas-strohmann:mainthomas-strohmann/RealAnalysisGame:mainCopy head branch name to clipboard