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 18 research declarations. Search 10,000 more complete Mathlib declarations.
18 results
Clear filtersCedar.Data.Map.mapMOnValues_ok_implies_all_ok
Plain-language statement
Note that the converse is not true: counterexample m₁ is [(1, false)], m₂ is [(1, false), (2, true)], f is Except.ok But for a limited converse, see all_ok_implies_mapMOnValues_ok
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mapMOnValues_preserves_keys
Plain-language statement
This is not stated in terms of Map.keys because Map.keys produces a Set, and we want the even stronger property that it not only preserves the key-set, but also the key-order. (We'll use this to prove mapMOnValues_some_wf.)
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mapMOnValues_some_implies_all_from_some_alt_proof
Plain-language statement
alternate proof of mapMOnValues_some_implies_all_from_some, which instead of relying on mapMOnValues_some_implies_forall₂, relies on List.mapM_some_implies_all_from_some. Which do we prefer?
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mapMOnValues_some_implies_all_some_alt_proof
Plain-language statement
alternate proof of mapMOnValues_some_implies_all_some, which instead of relying on mapMOnValues_some_implies_forall₂, relies on List.mapM_some_implies_all_some. Which do we prefer?
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mapMOnValues_some_wf_alt_proof
Plain-language statement
Alternate proof of mapMOnValues_some_wf, that relies on List.mapM_some_eq_filterMap instead of mapMOnValues_preserves_keys. Which do we prefer?
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Data.Map.mem_values_make
Plain-language statement
Very similar to mem_make_mem_list above
Source project: Cedar Specification
Person-level attribution pending.