OAI/Combinatorics/UniformKServer/RawMetric.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.RawMetric.present line 16
2. theorem OAI.UniformKServer.RawMetric.present_eq line 17
3. theorem OAI.UniformKServer.RawMetric.present_pos line 19
4. theorem OAI.UniformKServer.RawMetric.metric_key_inj line 23
5. theorem OAI.UniformKServer.RawMetric.represents line 32
6. theorem OAI.UniformKServer.RawMetric.bounds_ok line 40
7. theorem OAI.UniformKServer.RawMetric.horizon_eq line 63