OAI/Combinatorics/EditApproximation/Coarse/CoarseBinaryRead.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryRead_value line 13

   Source documentation

   Read one array cell; absent arrays represent exact zero.

    theorem coarseBinaryRead_value (array : CoarseBinaryArray) (i : ℕ) :
       (coarseBinaryRead array i).value = ((coarseBinaryContents array).getD [])[i]?.getD 0 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction.CoarseBinaryArray, OAI.EditApproximation.BinaryFraction.coarseBinaryRead, OAI.EditApproximation.BinaryFraction.value, OAI.EditApproximation.BinaryFraction.coarseBinaryContents

2. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryRead_rep line 24