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 1,591 to 1,596 of 2,569 results.
List.mapM_implies_forall₂
Mathematical 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
Mathematical statement
Same as mapM_implies_forall₂ but for Option
Source project: Cedar Specification
Person-level attribution pending.
List.mapM_preserves_SortedBy
Mathematical statement
mapM preserves SortedBy if the keys are preserved
Source project: Cedar Specification
Person-level attribution pending.
List.mapM'_error_implies_exists_error
Mathematical 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₂
Mathematical 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'
Mathematical 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.