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 200 research declarations. Search 10,000 more complete Mathlib declarations.
200 results
Clear filtersList.mapM_implies_forall₂
Plain-language statement
Introduces forall₂ through the input output relation of a f through List.mapM. This is slightly stronger than the forward direction of mapM_ok_iff_forall₂ since it allowed an extra x ∈ xs condition in h.
Source project: Cedar Specification
Person-level attribution pending.
List.mapM_implies_forall₂_option
Plain-language statement
Same as mapM_implies_forall₂ but for Option
Source project: Cedar Specification
Person-level attribution pending.
List.mapM_preserves_SortedBy
Plain-language statement
mapM preserves SortedBy if the keys are preserved
Source project: Cedar Specification
Person-level attribution pending.
List.mapM'_error_implies_exists_error
Plain-language statement
The converse is not true: counterexample xs is [1, 2] and f is Except.error. In that case, f 2 = .error 2 but xs.mapM' f = .error 1. But for a limited converse, see element_error_implies_mapM_error
Source project: Cedar Specification
Person-level attribution pending.
List.mapM'_some_iff_forall₂
Plain-language statement
Copy of mapM'_ok_iff_forall₂ but for option instead of exception
Source project: Cedar Specification
Person-level attribution pending.
List.mapUnion_union_mapUnion'
Plain-language statement
mapUnion_union_mapUnion applies when you have the same function f and different input lists. mapUnion_union_mapUnion' applies when you have different functions f/g and the same input list.
Source project: Cedar Specification
Person-level attribution pending.