OAI/Combinatorics/UniformKServer/ChronologicalRoster.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.ChronologicalRoster.age line 14

    Source documentation

    Ages count subsequent chronological insertions, whether or not those entries have retired. Equal physical centers remain distinct records.

    def age (S : Finset I) (c : I → X) (r : ℝ) (i : I) : ℕ :=
…
  2. def OAI.UniformKServer.ChronologicalRoster.young line 17
  3. theorem OAI.UniformKServer.ChronologicalRoster.local_age_count line 26
  4. theorem OAI.UniformKServer.ChronologicalRoster.age_insert line 51
  5. theorem OAI.UniformKServer.ChronologicalRoster.new_age_zero line 63
  6. theorem OAI.UniformKServer.ChronologicalRoster.ball_young_count line 73