OAI/Topology/CoarseAssembly/RoeLocalCompactness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local compactness on the actual discrete ample module

  1. def OAI.CoarseAssembly.DiscreteRoe.LocallyCompact line 18

    Source documentation

    The usual local-compactness condition, with the actual multiplication operators.

    def LocallyCompact (T : Operator X H) : Prop :=
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator

  2. theorem OAI.CoarseAssembly.DiscreteRoe.locallyCompact_of_compact_rows_columns line 24
  3. theorem OAI.CoarseAssembly.DiscreteRoe.locallyCompact_of_propagation line 38
  4. theorem OAI.CoarseAssembly.DiscreteRoe.generator_locallyCompact line 46