OAI/RingTheory/DirectFiniteness/DiagramReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KaplanskyCounterexample.Planar.OpenDiagram.related_iff line 14

   Source documentation

   Insertions and deletions preserve the existence of the anchored lifetime drawing.

   theorem OpenDiagram.related_iff (token : X × Bool → F × A)
       (Allowed : List (X × Bool) → Prop)
       (hA : ∀ r, Allowed r → ∃ v, (∀ t ∈ r.map token, Inc v t.1) ∧
         ((r.map token).map (fun t => ι v t.1 t.2)).sum = 0)
       {u w : List (X × Bool)} (h : WordReduction.Related Allowed u w) :
       Nonempty (OpenDiagram Inc ι f₀ (u.map token)) ↔
         Nonempty (OpenDiagram Inc ι f₀ (w.map token)) := by
   …

   Mentions: OAI.KaplanskyCounterexample.WordReduction.Related, OAI.KaplanskyCounterexample.Planar.OpenDiagram