OAI/Topology/CoarseAssembly/MultiplierBoundaryNearby.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Norm-local constancy of the actual Roe boundary class

  1. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass_eq_of_nearby line 16