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.Logic.HML.theoryEq_isBisimulation
Plain-language statement
Theory equivalence is a bisimulation.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Logic.PL.DerivableIn.cut_away
Plain-language statement
Remove unnecessary hypotheses. This can't be computable because it requires picking an order on the finset Δ.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Logic.PL.Theory.equiv_iff_equiv_derivableIn_hypothesis
Plain-language statement
A and B are equivalent (in T) iff they have the same strength as hypotheses.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LTS.Execution.comp
Plain-language statement
The composition of two executions is an execution.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LTS.Execution.to_mTr
Plain-language statement
Converts an execution into a multistep transition.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.LTS.IsBisimulation.traceEq_not_bisim
Plain-language statement
In general, trace equivalence is not a bisimulation (extra conditions are needed, see for example Bisimulation.deterministic_trace_eq_is_bisim).
Source project: Lean Computer Science Library
Person-level attribution pending.