OAI/Analysis/MarkovType/FinitelyRepresentable.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.FinitelyRepresentable line 12
2. def OAI.MarkovSuperreflexivity.CanonicallyReflexive line 19
3. theorem OAI.MarkovSuperreflexivity.FinitelyRepresentable.refl line 30
4. theorem OAI.MarkovSuperreflexivity.FinitelyRepresentable.of_subsingleton line 40
5. theorem OAI.MarkovSuperreflexivity.FinitelyRepresentable.target_linearIsometry line 47
6. theorem OAI.MarkovSuperreflexivity.FinitelyRepresentable.injective_of_lower_bound line 56
7. theorem OAI.MarkovSuperreflexivity.FinitelyRepresentable.compose_bounds line 64
8. theorem OAI.MarkovSuperreflexivity.FinitelyRepresentable.trans line 80