OAI/Geometry/PlaneColoring/GraphCuts.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.EuclideanFiveColor.graphEdgePoint_index line 10
2. lemma OAI.EuclideanFiveColor.graphRealization_positive_adj line 15
3. lemma OAI.EuclideanFiveColor.graphRealization_pair_le line 25
4. def OAI.EuclideanFiveColor.graphCutRealization line 31
5. abbrev OAI.EuclideanFiveColor.GraphCutSpace line 34
6. lemma OAI.EuclideanFiveColor.graphRealization_subset_cut line 35
7. lemma OAI.EuclideanFiveColor.graphCut_dominant line 44
8. lemma OAI.EuclideanFiveColor.graphCut_dominant_unique line 55
9. def OAI.EuclideanFiveColor.graphCutRetract line 61
10. lemma OAI.EuclideanFiveColor.graphCutRetract_tree line 63
11. lemma OAI.EuclideanFiveColor.graphCutRetract_dominant line 66
12. lemma OAI.EuclideanFiveColor.graphCutRetract_mem line 71
13. def OAI.EuclideanFiveColor.graphCutStub line 78

    Source documentation

    The closed half of a deleted edge, viewed inside the cut graph.

    def graphCutStub {V : Type u} (T : SimpleGraph V) (i j : V) : Set (GraphCutSpace T) :=
    …

    Mentions: OAI.EuclideanFiveColor.GraphCutSpace

14. lemma OAI.EuclideanFiveColor.graphCutStub_retract line 80
15. lemma OAI.EuclideanFiveColor.graphCut_cover line 96
16. lemma OAI.EuclideanFiveColor.graphCutStub_closed line 116
17. lemma OAI.EuclideanFiveColor.continuous_graphCutRetract line 122
18. lemma OAI.EuclideanFiveColor.graphMidpoint_coord_le line 143
19. lemma OAI.EuclideanFiveColor.graph_dominant_mem_cut line 147
20. lemma OAI.EuclideanFiveColor.graphEdgePoint_lerp_vertex line 155
21. lemma OAI.EuclideanFiveColor.graphCut_lerp_mem line 160
22. def OAI.EuclideanFiveColor.graphCutRetraction line 178
23. def OAI.EuclideanFiveColor.graphCutInclusion line 182
24. def OAI.EuclideanFiveColor.graphCutHomotopy line 185
25. theorem OAI.EuclideanFiveColor.graphCut_contractible line 197

    Source documentation

    Removing the non-tree edge midpoints leaves a contractible graph (tree with half-open stubs).

    theorem graphCut_contractible {V : Type u} [Fintype V] {T : SimpleGraph V} (hT : T.IsTree) :
        ContractibleSpace (GraphCutSpace T) := by
    …

    Mentions: OAI.EuclideanFiveColor.GraphCutSpace

26. def OAI.EuclideanFiveColor.FiberCrosses line 215

    Source documentation

    A compact connected fiber joins both designated boundary sets.

    def FiberCrosses {X : Type u} {Y : Type v} [TopologicalSpace X]
        (f : X → Y) (A B : Set X) (b : Y) : Prop :=
    …

27. lemma OAI.EuclideanFiveColor.fiberCrosses_symm line 219
28. lemma OAI.EuclideanFiveColor.compact_fiber_partition line 223
29. theorem OAI.EuclideanFiveColor.finite_fiber_separation line 269

    Source documentation

    All finitely many non-crossing bad fibers can simultaneously be separated, with the prescribed inner/outer closed sets on opposite sides.

    theorem finite_fiber_separation {X : Type u} {Y : Type v} [TopologicalSpace X]
        [TopologicalSpace Y] [CompactSpace X] [T2Space X] [T1Space Y]
        (f : C(X,Y)) {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) (hd : Disjoint A B)
        (S : Finset Y) (hn : ∀b∈S,¬FiberCrosses f A B b) :
        ∃C₀ C₁ : Set X, IsCompact C₀ ∧ IsCompact C₁ ∧ Disjoint C₀ C₁ ∧
          A⊆C₀ ∧ B⊆C₁ ∧ f ⁻¹' (↑S : Set Y)⊆C₀∪C₁ := by
    …

    Mentions: OAI.EuclideanFiveColor.FiberCrosses