OAI/Analysis/MarkovType/JamesEnflo.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_finiteTriangularObstruction line 14
2. theorem OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_iff_finiteTriangularObstruction line 19
3. theorem OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_hasEquivalentUSNorm line 24
4. theorem OAI.MarkovSuperreflexivity.HasEquivalentUCNorm.canonicallyReflexive_of_finitelyRepresentable line 29
5. theorem OAI.MarkovSuperreflexivity.exists_nonreflexive_finitelyRepresentable_of_not_hasEquivalentUCNorm line 35
6. theorem OAI.MarkovSuperreflexivity.hasEquivalentUCNorm_of_reflexive_finitelyRepresentable line 43