OAI/Combinatorics/EditApproximation/Geometry/SourceRankedKeys.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.SourceRanked.uncachedKeys_table_mem line 18

   Source documentation

   Forgetting source leaves preserves every table request, including those which the mixed memo execution first encounters after a cache hit.

   theorem uncachedKeys_table_mem (root item : κ)
       (hitem : Sum.inr item ∈ rankedUncachedKeys (rank tableRank)
         (body tableRank tableBody sourceValue) (.inr root)) :
       item ∈ rankedUncachedKeys tableRank (projectedBody tableRank tableBody sourceValue) root := by
   …

   Mentions: OAI.EditApproximation.rankedUncachedKeys, OAI.EditApproximation.SourceRanked.rank, OAI.EditApproximation.SourceRanked.body, OAI.EditApproximation.SourceRanked.projectedBody