OAI/Analysis/MarkovType/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.MarkovTypeWith.hasEquivalentUCNorm line 12
2. theorem OAI.MarkovSuperreflexivity.HasNontrivialMarkovType.hasEquivalentUCNorm line 19
3. theorem OAI.MarkovSuperreflexivity.HasMarkovType.two_hasEquivalentUCNorm line 24
4. theorem OAI.MarkovSuperreflexivity.HasEquivalentUCNorm.hasNontrivialMarkovType line 29
5. theorem OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm line 36

   Distinct definitions of this name: ComparatorChallenges/MarkovType.lean:71 (same statement text; different proof or body). Qualify references as OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm@path.