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 136 research declarations. Search 10,000 more complete Mathlib declarations.
136 results
Clear filtersCslib.LTS.OmegaExecution.flatten_mTr
Plain-language statement
Concatenating an infinite sequence of multistep transitions.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LTS.saturate_mTr_sMTr_not_nil_iff
Plain-language statement
A saturated multistep transition with a nonempty label list implies a multistep transition.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LTS.saturate_tr_saturate_sTr
Plain-language statement
In a saturated LTS, the transition and saturated transition relations are the same.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LTS.totalize.nonsink_mtr_iff
Plain-language statement
In totalize, the multistep transitions between non-sink states correspond exactly to the multistep transitions in the original LTS.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.MachineLearning.PACLearning.ae_mem_versionSpace_of_realizable
Plain-language statement
Under iid sampling from the realizable joint distribution induced by c ∈ C and a probability measure P on α, the target concept c lies in the version space almost surely.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.MachineLearning.PACLearning.empiricalError_eq_div
Plain-language statement
The empirical 0-1 error equals the empirical miscount divided by the sample size.
Source project: Lean Computer Science Library
Person-level attribution pending.