OAI/Analysis/LipschitzHilbert/Estimates/FiniteRestrictedStrongNull.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Null support-measure levels contribute zero and can be removed before the positive-measure class argument.

  1. theorem OAI.LipschitzHilbert.finite_restricted_strong_nonneg line 11