TopologyDynamics

Difficulty: hard — 6 definitions, 0 abbreviations, 1 lemmas, 2 theorems, 0 examples.

definition lemma theorem
legend
Topology.restrict (T : Topology) (S : Set T.Block) : Topology
Show details 
fun T S =>
  { Block := ↑S, Vertex := fun b => T.Vertex ↑b, internal := fun b => T.internal ↑b,
    external := SimpleGraph.induce S T.external, border := fun b => T.border ↑b,
    link := fun {x x_1} h => T.link ⋯ }

Complexity: 293 (size of the value term)

Outer dependencies: Topology

Mathlib dependencies: Set, Set.Elem, SimpleGraph.induce, SimpleGraph.induce_adj

Used by: (none)

SimpleGraph.induceComplSingletonEquiv {V : Type} (H : SimpleGraph V) (S : Set V) (b : ↑S) :
  SimpleGraph.induce {b}ᶜ (SimpleGraph.induce S H) ≃g SimpleGraph.induce (S \ {↑b}) H
Show details 
fun {V} H S b =>
  { toFun := fun x => ⟨↑↑x, ⋯⟩, invFun := fun x => ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
    map_rel_iff' := ⋯ }

Complexity: 961 (size of the value term)

Outer dependencies: (none)

Mathlib dependencies: Equiv, Set, Set.Elem, SimpleGraph, SimpleGraph.Iso, SimpleGraph.induce

Lean core dependencies: Iff.rfl, Not, Subtype, Subtype.ext, congrArg, rfl

Used by: Topology.leave_preserves_connected

Topology.Event (T : Topology) : Type
Show details 
| Topology.Event.idle : {T : Topology} → T.Event
| Topology.Event.join : {T : Topology} → T.Block → T.Event
| Topology.Event.leave : {T : Topology} → T.Block → T.Event

Outer dependencies: Topology

Lean core dependencies: Eq, HEq, Nat, Nat.ble, Nat.decEq, Not, PULift, cond, dite, eq_of_heq

Used by: Topology.Step.coverageFunctor, Topology.membership, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck, Topology.step, Topology.step_conserves, instNonemptyEvent, instNormEvent

Topology.Signal : Type
Show details 
| Topology.Signal.quiet : Topology.Signal
| Topology.Signal.left : Topology.Signal

Outer dependencies: (none)

Lean core dependencies: Eq, Nat, Nat.ble, PULift, cond, noConfusionEnum, noConfusionTypeEnum

Used by: Topology.Step.coverageFunctor, Topology.membership, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck, Topology.step, Topology.step_conserves, instNonemptySignal, instNormSignal

instNonemptyEvent {T : Topology} : Nonempty T.Event
Show details 
fun {T} => Nonempty.intro Topology.Event.idle

Complexity: 11 (size of the value term)

Outer dependencies: Topology, Topology.Event

Lean core dependencies: Nonempty

Used by: Topology.Step.coverageFunctor, Topology.membership, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck

instNonemptySignal : Nonempty Topology.Signal
Show details 
Nonempty.intro Topology.Signal.quiet

Complexity: 5 (size of the value term)

Outer dependencies: Topology.Signal

Lean core dependencies: Nonempty

Used by: Topology.Step.coverageFunctor, Topology.membership, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck

instNormEvent {T : Topology} : Norm T.Event
Show details 
fun {T} =>
  {
    norm := fun x =>
      match x with
      | Topology.Event.idle => 0
      | Topology.Event.join b => 1
      | Topology.Event.leave b => 0 }

Complexity: 69 (size of the value term)

Outer dependencies: Topology, Topology.Event

Mathlib dependencies: Norm, Real

Lean core dependencies: Unit, Unit.unit

Used by: Topology.Step.coverageFunctor, Topology.membership, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck, Topology.step_conserves

instNormSignal : Norm Topology.Signal
Show details 
{
  norm := fun x =>
    match x with
    | Topology.Signal.quiet => 0
    | Topology.Signal.left => 1 }

Complexity: 41 (size of the value term)

Outer dependencies: Topology.Signal

Mathlib dependencies: Norm, Real

Lean core dependencies: Unit, Unit.unit

Used by: Topology.Step.coverageFunctor, Topology.membership, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck, Topology.step_conserves

instNormSetBlock {T : Topology} : Norm (Set T.Block)
Show details 
fun {T} => { norm := fun S => ↑S.ncard }

Complexity: 29 (size of the value term)

Outer dependencies: Topology

Mathlib dependencies: Norm, Real, Set, Set.ncard

Lean core dependencies: Nat.cast

Used by: Topology.Step.coverageFunctor, Topology.membership, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck, Topology.step_conserves

Topology.step (T : Topology) (S : Set T.Block) (e : T.Event) : Set T.Block × Topology.Signal
Show details 
fun T S e =>
  match e with
  | Topology.Event.idle => (S, Topology.Signal.quiet)
  | Topology.Event.join b =>
    if b ∈ S then (S, Topology.Signal.left) else (insert b S, Topology.Signal.quiet)
  | Topology.Event.leave b =>
    if b ∈ S then (S \ {b}, Topology.Signal.left) else (S, Topology.Signal.quiet)

Complexity: 281 (size of the value term)

Outer dependencies: Topology, Topology.Event, Topology.Signal

Mathlib dependencies: Set

Lean core dependencies: Classical.propDecidable, Prod, Unit, ite

Used by: Topology.Step.coverageFunctor, Topology.membership, Topology.step_conserves

Topology.step_conserves (T : Topology) [Fintype T.Block] (S : Set T.Block) (e : T.Event) :
  ‖S‖ + ‖e‖ = ‖(T.step S e).1‖ + ‖(T.step S e).2‖
Show details 
fun T [Fintype T.Block] S e =>
  Topology.Event.casesOn (motive := fun t =>
    e = t → ‖S‖ + ‖e‖ = ‖(T.step S e).1‖ + ‖(T.step S e).2‖) e
    (fun h => Eq.symm h ▸ Eq.refl (‖S‖ + ‖Topology.Event.idle‖))
    (fun b h =>
      Eq.symm h ▸
        if hb : b ∈ S then
          Eq.mpr
            (id
              (congrArg (fun _a => ‖S‖ + ‖Topology.Event.join b‖ = ‖_a.1‖ + ‖_a.2‖)
                (Topology.step.eq_2 T S b)))
            (Eq.mpr
              (id
                (congrArg (fun _a => ‖S‖ + ‖Topology.Event.join b‖ = ‖_a.1‖ + ‖_a.2‖) (if_pos hb)))
              (id
                (Mathlib.Tactic.Ring.of_eq
                  (Mathlib.Tactic.Ring.Common.add_congr
                    (Mathlib.Tactic.Ring.Common.atom_pf (↑S.ncard) rfl
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              ↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                ↑S.ncard ^ Nat.rawCast 1 * _a)
                            (Eq.symm rfl)))
                        (Eq.refl (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                    (Mathlib.Tactic.Ring.Common.add_pf_add_gt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                        (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                  (Mathlib.Tactic.Ring.Common.add_congr
                    (Mathlib.Tactic.Ring.Common.atom_pf (↑S.ncard) rfl
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              ↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                ↑S.ncard ^ Nat.rawCast 1 * _a)
                            (Eq.symm rfl)))
                        (Eq.refl (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                    (Mathlib.Tactic.Ring.Common.add_pf_add_gt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                        (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))))
        else
          Eq.mpr
            (id
              (congrArg (fun _a => ‖S‖ + ‖Topology.Event.join b‖ = ‖_a.1‖ + ‖_a.2‖)
                (Topology.step.eq_2 T S b)))
            (Eq.mpr
              (id
                (congrArg (fun _a => ‖S‖ + ‖Topology.Event.join b‖ = ‖_a.1‖ + ‖_a.2‖) (if_neg hb)))
              (id
                (Eq.mpr
                  (id
                    (congrArg (fun _a => ↑S.ncard + 1 = ↑_a + 0)
                      (Set.ncard_insert_of_notMem hb (Set.toFinite S))))
                  (Eq.mpr
                    (id
                      (congrArg (Eq (↑S.ncard + 1))
                        (congrFun'
                          (congrArg HAdd.hAdd
                            (Eq.trans (Nat.cast_add S.ncard 1)
                              (congrArg (HAdd.hAdd ↑S.ncard) Nat.cast_one)))
                          0)))
                    (Mathlib.Tactic.Ring.of_eq
                      (Mathlib.Tactic.Ring.Common.add_congr
                        (Mathlib.Tactic.Ring.Common.atom_pf (↑S.ncard) rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ↑S.ncard ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.cast_pos
                          (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Tactic.Ring.Common.add_pf_add_gt (Nat.rawCast 1)
                          (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                            (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                      (Mathlib.Tactic.Ring.Common.add_congr
                        (Mathlib.Tactic.Ring.Common.add_congr
                          (Mathlib.Tactic.Ring.Common.atom_pf (↑S.ncard) rfl
                            (Eq.mpr
                              (id
                                (congrArg
                                  (fun _a =>
                                    ↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                      ↑S.ncard ^ Nat.rawCast 1 * _a)
                                  (Eq.symm rfl)))
                              (Eq.refl (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1))))
                          (Mathlib.Tactic.Ring.cast_pos
                            (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Tactic.Ring.Common.add_pf_add_gt (Nat.rawCast 1)
                            (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                              (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                        (Mathlib.Tactic.Ring.cast_zero
                          (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                        (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                          (Nat.rawCast 1 + (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))))))))
    (fun b h =>
      Eq.symm h ▸
        if hb : b ∈ S then
          Eq.mpr
            (id
              (congrArg (fun _a => ‖S‖ + ‖Topology.Event.leave b‖ = ‖_a.1‖ + ‖_a.2‖)
                (Topology.step.eq_3 T S b)))
            (Eq.mpr
              (id
                (congrArg (fun _a => ‖S‖ + ‖Topology.Event.leave b‖ = ‖_a.1‖ + ‖_a.2‖) (if_pos hb)))
              (id
                (Eq.mpr
                  (id
                    (congrArg (fun _a => ↑S.ncard + 0 = ↑_a + 1)
                      (Set.ncard_sdiff_singleton_of_mem hb)))
                  (have h1 := (Set.ncard_pos (Set.toFinite S)).mpr (Exists.intro b hb);
                  Eq.mpr
                    (id
                      (congrArg (Eq (↑S.ncard + 0))
                        (congrFun'
                          (congrArg HAdd.hAdd
                            (Eq.trans
                              ((fun x_0 x_1 => (fun x_0 x_1 => Nat.cast_sub h1) x_0 x_1) ℝ
                                Real.instRing.toAddGroupWithOne)
                              (congrArg (HSub.hSub ↑S.ncard) Nat.cast_one)))
                          1)))
                    (Mathlib.Tactic.Ring.of_eq
                      (Mathlib.Tactic.Ring.Common.add_congr
                        (Mathlib.Tactic.Ring.Common.atom_pf (↑S.ncard) rfl
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  ↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                    ↑S.ncard ^ Nat.rawCast 1 * _a)
                                (Eq.symm rfl)))
                            (Eq.refl (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1))))
                        (Mathlib.Tactic.Ring.cast_zero
                          (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                        (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                          (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
                      (Mathlib.Tactic.Ring.Common.add_congr
                        (Mathlib.Tactic.Ring.Common.sub_congr
                          (Mathlib.Tactic.Ring.Common.atom_pf (↑S.ncard) rfl
                            (Eq.mpr
                              (id
                                (congrArg
                                  (fun _a =>
                                    ↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                      ↑S.ncard ^ Nat.rawCast 1 * _a)
                                  (Eq.symm rfl)))
                              (Eq.refl (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1))))
                          (Mathlib.Tactic.Ring.cast_pos
                            (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                          (Mathlib.Tactic.Ring.Common.sub_pf
                            (Mathlib.Tactic.Ring.Common.neg_add
                              (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                                (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg)
                                  (Mathlib.Meta.NormNum.IsNat.to_isInt
                                    (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                                  (Eq.refl (Int.negOfNat 1))))
                              Mathlib.Tactic.Ring.Common.neg_zero)
                            (Mathlib.Tactic.Ring.Common.add_pf_add_gt (Int.negOfNat 1).rawCast
                              (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                                (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                        (Mathlib.Tactic.Ring.cast_pos
                          (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one))
                        (Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero
                          (Mathlib.Meta.NormNum.IsInt.to_isNat
                            (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt
                                (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1))
                              (Eq.refl (Int.ofNat 0))))
                          (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                            (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))))))
        else
          Eq.mpr
            (id
              (congrArg (fun _a => ‖S‖ + ‖Topology.Event.leave b‖ = ‖_a.1‖ + ‖_a.2‖)
                (Topology.step.eq_3 T S b)))
            (Eq.mpr
              (id
                (congrArg (fun _a => ‖S‖ + ‖Topology.Event.leave b‖ = ‖_a.1‖ + ‖_a.2‖) (if_neg hb)))
              (id
                (Mathlib.Tactic.Ring.of_eq
                  (Mathlib.Tactic.Ring.Common.add_congr
                    (Mathlib.Tactic.Ring.Common.atom_pf (↑S.ncard) rfl
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              ↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                ↑S.ncard ^ Nat.rawCast 1 * _a)
                            (Eq.symm rfl)))
                        (Eq.refl (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1))))
                    (Mathlib.Tactic.Ring.cast_zero
                      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                    (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                      (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.Common.add_congr
                    (Mathlib.Tactic.Ring.Common.atom_pf (↑S.ncard) rfl
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              ↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 =
                                ↑S.ncard ^ Nat.rawCast 1 * _a)
                            (Eq.symm rfl)))
                        (Eq.refl (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1))))
                    (Mathlib.Tactic.Ring.cast_zero
                      (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero))
                    (Mathlib.Tactic.Ring.Common.add_pf_add_zero
                      (↑S.ncard ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))))
    (Eq.refl e)

Complexity: 41620 (size of the value term)

Dependencies: Topology, Topology.Event, Topology.Signal, Topology.step, instNormEvent, instNormSetBlock, instNormSignal

Mathlib dependencies: AddGroupWithOne, Fintype, Int.rawCast, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isInt_add, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.atom_pf, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Tactic.Ring.Common.neg_zero, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.sub_pf, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.Ring.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.cast_add, Nat.cast_one, Nat.cast_sub, Nat.cast_zero, Nat.rawCast, Real, Ring, Set, Set.Nonempty, Set.ncard, Set.ncard_insert_of_notMem, Set.ncard_pos, Set.ncard_sdiff_singleton_of_mem, Set.toFinite

Lean core dependencies: Classical.propDecidable, Eq, Eq.mpr, Eq.symm, Eq.trans, Int, Int.negOfNat, Nat, Nat.cast, Not, Prod, congrArg, congrFun', dite, id, if_neg, if_pos, inferInstance, ite, rfl

Used by: Topology.Step.coverageFunctor, Topology.membership

Topology.membership (T : Topology) [Fintype T.Block] :
  InformationSystem (Set T.Block) T.Event Topology.Signal
Show details 
fun T [Fintype T.Block] => { step := T.step, conserves := ⋯ }

Complexity: 51 (size of the value term)

Outer dependencies: InformationSystem, Topology, Topology.Event, Topology.Signal, instNonemptyEvent, instNonemptySignal, instNormEvent, instNormSetBlock, instNormSignal

Inner dependencies: Topology.step, Topology.step_conserves

Mathlib dependencies: Fintype, Set

Used by: Topology.Step.coverageFunctor, Topology.runArrows, Topology.runArrows', Topology.runGrothendieck

graph
Topology.join_preserves_connected (T : Topology) {S : Set T.Block}
  (h_conn : (SimpleGraph.induce S T.external).Connected) {b b' : T.Block} (hb' : b' ∈ S)
  (hadj : T.external.Adj b b') : (SimpleGraph.induce (insert b S) T.external).Connected
Show details 
fun T {S} h_conn {b b'} hb' hadj =>
  have hunion :=
    SimpleGraph.induce_union_connected h_conn.preconnected
      (SimpleGraph.induce_pair_connected_of_adj hadj).preconnected
      (Exists.intro b'
        ⟨hb',
          of_eq_true
            (Eq.trans Set.mem_insert_iff._simp_1
              (Eq.trans
                (congrArg (Or (b' = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self b')))
                (or_true (b' = b))))⟩);
  have heq :=
    Set.ext fun x =>
      Eq.mpr
        (id
          (congr
            (congrArg Iff
              (Eq.trans (Topology.join_preserves_connected._simp_1_1 x S {b, b'})
                (congrArg (Or (x ∈ S))
                  (Eq.trans Topology.join_preserves_connected._simp_1_2
                    (congrArg (Or (x = b)) Topology.join_preserves_connected._simp_1_3)))))
            Topology.join_preserves_connected._simp_1_2))
        {
          mp := fun a =>
            Or.casesOn a (fun hx => Or.inr hx) fun h =>
              Or.casesOn h (fun hx => Or.inl hx) fun hx => Or.inr (Eq.symm hx ▸ hb'),
          mpr := fun a => Or.casesOn a (fun hx => Or.inr (Or.inl hx)) fun hx => Or.inl hx };
  Eq.mp (congrArg (fun _a => (SimpleGraph.induce _a T.external).Connected) heq) hunion

Complexity: 3729 (size of the value term)

Dependencies: Topology

Mathlib dependencies: Set, Set.Elem, Set.ext, Set.mem_insert_iff, Set.mem_singleton_iff, Set.mem_union, SimpleGraph.Connected, SimpleGraph.induce, SimpleGraph.induce_pair_connected_of_adj, SimpleGraph.induce_union_connected

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Iff, Or, True, congr, congrArg, eq_self, id, of_eq_true, or_true

Used by: (none)

Topology.leave_preserves_connected (T : Topology) {S : Set T.Block}
  (h_conn : (SimpleGraph.induce S T.external).Connected) (b : ↑S)
  [Fintype ↑((SimpleGraph.induce S T.external).neighborSet b)]
  (hdeg : (SimpleGraph.induce S T.external).degree b = 1) :
  (SimpleGraph.induce (S \ {↑b}) T.external).Connected
Show details 
fun T {S} h_conn b [Fintype ↑((SimpleGraph.induce S T.external).neighborSet b)] hdeg =>
  (SimpleGraph.Iso.connected_iff (T.external.induceComplSingletonEquiv S b)).mp
    (SimpleGraph.Connected.induce_compl_singleton_of_degree_eq_one h_conn hdeg)

Complexity: 749 (size of the value term)

Dependencies: Topology

Proof dependencies: SimpleGraph.induceComplSingletonEquiv

Mathlib dependencies: Fintype, Set, Set.Elem, SimpleGraph.Connected, SimpleGraph.Connected.induce_compl_singleton_of_degree_eq_one, SimpleGraph.Iso.connected_iff, SimpleGraph.degree, SimpleGraph.induce, SimpleGraph.neighborSet

Lean core dependencies: Eq, Nat

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