OAI/Probability/CriticalZ3/LatticePaths.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.CriticalZ3.Model line 12
  2. abbrev OAI.CriticalZ3.Model.Bit line 15
  3. abbrev OAI.CriticalZ3.Model.Config line 18
  4. instance OAI.CriticalZ3.Model.(instance at line 19) line 19
  5. instance OAI.CriticalZ3.Model.(instance at line 20) line 20
  6. def OAI.CriticalZ3.Box.bits line 24
  7. def OAI.CriticalZ3.LatticeGraph.bits line 31
  8. def OAI.CriticalZ3.LatticeGraph.Open line 35
  9. def OAI.CriticalZ3.LatticeGraph.Adj line 39
  10. def OAI.CriticalZ3.LatticeGraph.Conn line 43
  11. def OAI.CriticalZ3.LatticeGraph.Meets line 47
  12. theorem OAI.CriticalZ3.LatticeGraph.conn_iff line 50
  13. theorem OAI.CriticalZ3.LatticeGraph.adj_open line 56
  14. theorem OAI.CriticalZ3.LatticeGraph.adj_neighbor line 62
  15. theorem OAI.CriticalZ3.LatticeGraph.adj_symm line 68
  16. theorem OAI.CriticalZ3.LatticeGraph.conn_open line 74
  17. theorem OAI.CriticalZ3.LatticeGraph.conn_symm line 82
  18. theorem OAI.CriticalZ3.LatticeGraph.conn_trans line 91
  19. theorem OAI.CriticalZ3.LatticeGraph.conn_adj line 96
  20. theorem OAI.CriticalZ3.LatticeGraph.conn_determined line 99
  21. theorem OAI.CriticalZ3.LatticeGraph.meets_determined line 106
  22. theorem OAI.CriticalZ3.LatticeGraph.measurableSet_meets line 112
  23. theorem OAI.CriticalZ3.LatticeGraph.failure_comparison line 117
  24. def OAI.CriticalZ3.LatticeGraph.ContainsBox line 126
  25. theorem OAI.CriticalZ3.LatticeGraph.containsBox_node line 128
  26. theorem OAI.CriticalZ3.LatticeGraph.neighbor_incidence line 131
  27. theorem OAI.CriticalZ3.LatticeGraph.incidence_internal line 137
  28. theorem OAI.CriticalZ3.LatticeGraph.open_box_adj line 144
  29. theorem OAI.CriticalZ3.LatticeGraph.lift_path line 156

    Source documentation

    Lifting a vertex path into a finite graph, retaining the exact endpoints.

    theorem lift_path {r : Vertex → Vertex → Prop} {s : G.Node → G.Node → Prop}
    (hmem : ∀ x y, r x y → y ∈ G.vertices)
    (hrel : ∀ (x y : G.Node), r x.1 y.1 → s x y)
    {x y : G.Node} (h : Relation.ReflTransGen r x.1 y.1) : Relation.ReflTransGen s x y := by
…

    Mentions: OAI.CriticalZ3.Vertex

  30. theorem OAI.CriticalZ3.LatticeGraph.open_box_conn line 174