OAI/Analysis/StrictMeans/IndexConservation.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.StrictInverseFirstPower.Grid.discreteDivergenceline 11 - lemma
OAI.StrictInverseFirstPower.Grid.finite_support_shiftline 13 - lemma
OAI.StrictInverseFirstPower.Grid.finite_support_discreteDivergenceline 17 - lemma
OAI.StrictInverseFirstPower.Grid.finsum_discreteDivergenceline 20 - lemma
OAI.StrictInverseFirstPower.Grid.finite_rank_differenceline 27 - lemma
OAI.StrictInverseFirstPower.Grid.finite_top_differenceline 38 - lemma
OAI.StrictInverseFirstPower.Grid.meshIndex_difference_decompositionline 51 - lemma
OAI.StrictInverseFirstPower.Grid.meshIndex_change_finsum_zeroline 65