OAI/Analysis/MarkovType/SeminormUltralimit.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MarkovSuperreflexivity.seminormULimline 16 - theorem
OAI.MarkovSuperreflexivity.seminormULim_applyline 33 - theorem
OAI.MarkovSuperreflexivity.seminormULim_leline 37 - theorem
OAI.MarkovSuperreflexivity.le_seminormULimline 43 - theorem
OAI.MarkovSuperreflexivity.seminormULim_definiteline 49