Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 607 to 612 of 2,569 results.
Cslib.FLP.FairScheduler.fairDeliverMsg_scheduleMsgs
Mathematical statement
The correctness of d.scheduleMsgs ps s under the assumption a.FairDeliverMsg d ps q.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.FairScheduler.flatten_fairSegs
Mathematical statement
Given an infinite sequence of non-empty finite executions of algorithm a, if all messages with destinations in ps that are in-flight at the beginning of each finite execution are delivered in that finite execution, then those finite executions can be concatenated into an infinite execution of a in which every process in ps is fair.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.ZeroFaultAlg.left_leadsTo_right
Mathematical statement
Whenever the message carrying the input value for process 0 is enabled in a state, a message carrying that value is eventually sent to every process p by process 0.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.ZeroFaultAlg.right_leadsTo_out
Mathematical statement
Whenever a message carrying a value sent by process 0 is enabled at a process p, p eventually decides on that value.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.infinite_graph_ramsey
Mathematical statement
If the edges of an infinite complete graph is assigned a finite number of colors, then there must exist a color c and an infinite set s of vertices such that the edge between any two vertices of s is assigned the same color c.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LambdaCalculus.LocallyNameless.Fsub.Sub.map_subst
Mathematical statement
Subtyping of substitutions.
Source project: Lean Computer Science Library
Person-level attribution pending.