OAI/Topology/ArtinGroups/ParabolicIntersections/EmptyPlacement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The empty-placement lemma (Lemma 7.3 of paper 082-03).

  1. theorem OAI.HarmonicArtin.ParabolicIntersections.empty_placement_of_mesh line 14

    Source documentation

    Exact vertex tests on a spherical interval force a gap after at most N placements per occupied layer. Only the abstract published path identity is assumed; the layer-removal argument is proved here.

    theorem empty_placement_of_mesh (U : Set V) (hmesh : MeshNilpotent Q U) :
    ∃ N : ℕ, 0 < N ∧ ∀ (I : Type) [Fintype I] (E : BasedComplex Q (K := ℂ) I),
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent