Topology

Difficulty: moderate — 2 definitions, 0 abbreviations, 4 lemmas, 1 theorems, 0 examples.

definition lemma theorem
legend
Topology.whole (T : Topology) : SimpleGraph ((b : T.Block) × T.Vertex b)
Show details 
fun T =>
  SimpleGraph.fromRel fun x y =>
    match x, y with
    | ⟨b, v⟩, ⟨c, w⟩ =>
      (∃ (h : b = c), (T.internal b).Adj v (⋯ ▸ w)) ∨
        ∃ (h : T.external.Adj b c), ↑(T.link h).1 = v ∧ ↑(T.link h).2 = w

Complexity: 403 (size of the value term)

Outer dependencies: Topology

Mathlib dependencies: SimpleGraph, SimpleGraph.fromRel

Lean core dependencies: And, Eq, Eq.symm, Exists, Or, Sigma, Subtype

Used by: Topology.whole_adj_of_internal, Topology.whole_adj_of_link, Topology.whole_connected, Topology.whole_reachable_of_external, Topology.whole_reachable_of_internal

Topology.whole_adj_of_internal (T : Topology) {b : T.Block} {v w : T.Vertex b}
  (h : (T.internal b).Adj v w) : T.whole.Adj ⟨b, v⟩ ⟨b, w⟩
Show details 
fun T {b} {v w} h =>
  have hne := SimpleGraph.ne_of_adj (T.internal b) h;
  Eq.mpr (id (congrArg (fun _a => _a.Adj ⟨b, v⟩ ⟨b, w⟩) (Topology.whole.eq_1 T)))
    (Eq.mpr
      (id
        (congrArg (fun _a => _a)
          (propext
            (SimpleGraph.fromRel_adj
              (fun x y =>
                match x, y with
                | ⟨b, v⟩, ⟨c, w⟩ =>
                  (∃ (h : b = c), (T.internal b).Adj v (Topology.whole._proof_1 T b c h ▸ w)) ∨
                    ∃ (h : T.external.Adj b c), ↑(T.link h).1 = v ∧ ↑(T.link h).2 = w)
              ⟨b, v⟩ ⟨b, w⟩))))
      ⟨fun heq =>
        hne
          (Eq.mp
            (Eq.trans (Sigma.mk.injEq b v b w)
              (Eq.trans (congr (congrArg And (eq_self b)) (heq_eq_eq v w)) (true_and (v = w))))
            heq),
        Or.inl (Or.inl (Exists.intro rfl h))⟩)

Complexity: 9710 (size of the value term)

Dependencies: Topology, Topology.whole

Mathlib dependencies: SimpleGraph, SimpleGraph.fromRel, SimpleGraph.fromRel_adj, SimpleGraph.ne_of_adj

Lean core dependencies: And, Eq, Eq.mp, Eq.mpr, Eq.trans, Exists, HEq, Ne, Or, Sigma, Subtype, True, congr, congrArg, eq_self, heq_eq_eq, id, rfl, true_and

Used by: Topology.whole_reachable_of_internal

Topology.whole_reachable_of_internal (T : Topology) {b : T.Block} {v w : T.Vertex b}
  (h : (T.internal b).Reachable v w) : T.whole.Reachable ⟨b, v⟩ ⟨b, w⟩
Show details 
fun T {b} {v w} h =>
  Nonempty.casesOn h fun p =>
    SimpleGraph.Walk.rec (fun {u} => SimpleGraph.Reachable.refl ⟨b, u⟩)
      (fun {u v w} hadj p ih =>
        SimpleGraph.Reachable.trans
          (SimpleGraph.Adj.reachable (Topology.whole_adj_of_internal T hadj)) ih)
      p

Complexity: 589 (size of the value term)

Dependencies: Topology, Topology.whole

Proof dependencies: Topology.whole_adj_of_internal

Mathlib dependencies: SimpleGraph.Reachable, SimpleGraph.Reachable.refl, SimpleGraph.Reachable.trans, SimpleGraph.Walk

Lean core dependencies: Sigma

Used by: Topology.whole_reachable_of_external

Topology.whole_reachable_of_external (T : Topology)
  (h_internal : ∀ (b : T.Block), (T.internal b).Connected) {b c : T.Block}
  (h : T.external.Reachable b c) (v : T.Vertex b) (w : T.Vertex c) : T.whole.Reachable ⟨b, v⟩ ⟨c, w⟩
Show details 
fun T h_internal {b c} h v w =>
  Nonempty.casesOn h fun p =>
    SimpleGraph.Walk.rec (motive := fun {b c} p =>
      ∀ (v : T.Vertex b) (w : T.Vertex c), T.whole.Reachable ⟨b, v⟩ ⟨c, w⟩)
      (fun {u} v w => Topology.whole_reachable_of_internal T ((h_internal u).preconnected v w))
      (fun {b d e} hadj p' ih v w =>
        have h1 :=
          Topology.whole_reachable_of_internal T ((h_internal b).preconnected v ↑(T.link hadj).1);
        have h2 := Topology.whole_adj_of_link T hadj;
        SimpleGraph.Reachable.trans h1
          (SimpleGraph.Reachable.trans (SimpleGraph.Adj.reachable h2) (ih (↑(T.link hadj).2) w)))
      p v w

Complexity: 1687 (size of the value term)

Dependencies: Topology, Topology.whole

Proof dependencies: Topology.whole_adj_of_link, Topology.whole_reachable_of_internal

Mathlib dependencies: SimpleGraph.Connected, SimpleGraph.Reachable, SimpleGraph.Reachable.trans, SimpleGraph.Walk

Lean core dependencies: Sigma, Subtype

Used by: Topology.whole_connected

graph
Topology.whole_connected (T : Topology) (h_internal : ∀ (b : T.Block), (T.internal b).Connected)
  (h_external : T.external.Connected) : T.whole.Connected
Show details 
fun T h_internal h_external =>
  Nonempty.casesOn h_external.nonempty fun b =>
    Nonempty.casesOn (h_internal b).nonempty fun v =>
      {
        preconnected := fun x y =>
          Topology.whole_reachable_of_external T h_internal (h_external.preconnected x.fst y.fst)
            x.snd y.snd,
        nonempty := Nonempty.intro ⟨b, v⟩ }

Complexity: 359 (size of the value term)

Dependencies: Topology, Topology.whole

Proof dependencies: Topology.whole_reachable_of_external

Mathlib dependencies: SimpleGraph.Connected

Lean core dependencies: Nonempty, Sigma

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend