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 filtersCedar.Thm.action_scope_produces_boolean
Plain-language statement
Lemma: evaluating the actionScope of any policy produces a boolean (and does not error)
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.allowed_iff_explicitly_permitted_and_not_denied
Plain-language statement
A request is allowed if and only if it is explicitly permitted and is not explicitly forbidden.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.allowed_only_if_explicitly_permitted
Plain-language statement
A request is allowed only if it is explicitly permitted.
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.alwaysMatchesOpt?_eqv_alwaysMatches?
Plain-language statement
Full equivalence for alwaysMatches? and alwaysMatchesOpt?, including both the .ok and .error cases
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.ancsUDF_app
Plain-language statement
Simplifies SymEntityData.ofActionType.ancsUDF
Source project: Cedar Specification
Person-level attribution pending.
Cedar.Thm.and_produces_bool_or_error
Plain-language statement
Every and expression produces either .ok bool or .error
Source project: Cedar Specification
Person-level attribution pending.