OAI/Geometry/RCD/Harmonic/TransverseBarrierLower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Positive inner mass of the transverse barrier

  1. theorem OAI.RegularPointCoordinates.transverse_barrier_pointwise_lower line 12
  2. theorem OAI.RegularPointCoordinates.transverse_barrier_integral_lower line 23