ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.bypass.length ≤ p.length
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.length ≤ p.bypass.length<GOAL>p.bypass = p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.bypass.support ⊆ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(↑p.toPath).support ⊆ p.support
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.bypass.darts ⊆ p.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>p.bypass.edges ⊆ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(↑p.toPath).darts ⊆ p.darts
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(↑p.toPath).edges ⊆ p.edges
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v : V<VAR>p : G.Walk u v<VAR>hinj : Function.Injective ⇑f<VAR>hp : p.IsPath<GOAL>(SimpleGraph.Walk.map f p).IsPath
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v : V<VAR>p : G.Walk u v<VAR>f : G →g G'<VAR>hp : (SimpleGraph.Walk.map f p).IsPath<GOAL>p.IsPath
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v : V<VAR>p : G.Walk u v<VAR>hinj : Function.Injective ⇑f<GOAL>(SimpleGraph.Walk.map f p).IsPath ↔ p.IsPath
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u v : V<VAR>p : G.Walk u v<VAR>hinj : Function.Injective ⇑f<GOAL>(SimpleGraph.Walk.map f p).IsTrail ↔ p.IsTrail
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>u : V<VAR>p : G.Walk u u<VAR>hinj : Function.Injective ⇑f<GOAL>(SimpleGraph.Walk.map f p).IsCycle ↔ p.IsCycle
<VAR>V : Type u<VAR>G G' : SimpleGraph V<VAR>h : G ≤ G'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(SimpleGraph.Walk.mapLe h p).IsTrail ↔ p.IsTrail
<VAR>V : Type u<VAR>G G' : SimpleGraph V<VAR>h : G ≤ G'<VAR>u v : V<VAR>p : G.Walk u v<GOAL>(SimpleGraph.Walk.mapLe h p).IsPath ↔ p.IsPath
<VAR>V : Type u<VAR>G G' : SimpleGraph V<VAR>h : G ≤ G'<VAR>u : V<VAR>p : G.Walk u u<GOAL>(SimpleGraph.Walk.mapLe h p).IsCycle ↔ p.IsCycle
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>hinj : Function.Injective ⇑f<VAR>u v : V<VAR>p : G.Path u v<GOAL>↑(SimpleGraph.Path.map f hinj p) = SimpleGraph.Walk.map f ↑p
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>hinj : Function.Injective ⇑f<VAR>u v : V<GOAL>Function.Injective (SimpleGraph.Path.map f hinj)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G ↪g G'<VAR>u v : V<VAR>p : G.Path u v<GOAL>↑(SimpleGraph.Path.mapEmbedding f p) = SimpleGraph.Walk.map f.toHom ↑p
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G ↪g G'<VAR>u v : V<GOAL>Function.Injective (SimpleGraph.Path.mapEmbedding f)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>H : SimpleGraph V<VAR>p : G.Walk u v<VAR>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<VAR>pp : p.IsPath<GOAL>(p.transfer H hp).IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<VAR>H : SimpleGraph V<VAR>q : G.Walk u u<VAR>qc : q.IsCycle<VAR>hq : ∀ e ∈ q.edges, e ∈ H.edgeSet<GOAL>(q.transfer H hq).IsCycle
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>s : Set (Sym2 V)<VAR>p : G.Walk v w<VAR>h : p.IsPath<VAR>hp : ∀ e ∈ p.edges, e ∉ s<GOAL>(SimpleGraph.Walk.toDeleteEdges s p hp).IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<VAR>s : Set (Sym2 V)<VAR>p : G.Walk v v<VAR>h : p.IsCycle<VAR>hp : ∀ e ∈ p.edges, e ∉ s<GOAL>(SimpleGraph.Walk.toDeleteEdges s p hp).IsCycle
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v u u' v' : V<VAR>s : Set (Sym2 V)<VAR>p : G.Walk u v<VAR>hu : u = u'<VAR>hv : v = v'<VAR>h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s<GOAL>SimpleGraph.Walk.toDeleteEdges s (p.copy hu hv) h = (SimpleGraph.Walk.toDeleteEdges s p ⋯).copy hu hv
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.Reachable u v ↔ Set.univ.Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>¬G.Reachable u v ↔ IsEmpty (G.Walk u v)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>p : Prop<VAR>u v : V<VAR>h : G.Reachable u v<VAR>hp : G.Walk u v → p<GOAL>p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>p : Prop<VAR>u v : V<VAR>h : G.Reachable u v<VAR>hp : G.Path u v → p<GOAL>p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>G.Reachable u v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.Adj u v<GOAL>G.Reachable u v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u : V<GOAL>G.Reachable u u
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<VAR>huv : G.Reachable u v<GOAL>G.Reachable v u
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.Reachable u v ↔ G.Reachable v u
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>huv : G.Reachable u v<VAR>hvw : G.Reachable v w<GOAL>G.Reachable u w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v
<VAR>V : Type u<VAR>V' : Type v<VAR>u v : V<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>f : G →g G'<VAR>h : G.Reachable u v<GOAL>G'.Reachable (f u) (f v)
<VAR>V : Type u<VAR>u v : V<VAR>G G' : SimpleGraph V<VAR>h : G ≤ G'<VAR>Guv : G.Reachable u v<GOAL>G'.Reachable u v
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>φ : G ≃g G'<VAR>u v : V<GOAL>G'.Reachable (φ u) (φ v) ↔ G.Reachable u v
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>φ : G ≃g G'<VAR>u : V<VAR>v : V'<GOAL>G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u)
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>Equivalence G.Reachable
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>H : SimpleGraph V'<VAR>f : G →g H<VAR>hf : Function.Surjective ⇑f<VAR>hG : G.Preconnected<GOAL>H.Preconnected
<VAR>V : Type u<VAR>G G' : SimpleGraph V<VAR>h : G ≤ G'<VAR>hG : G.Preconnected<GOAL>G'.Preconnected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>H : SimpleGraph V'<VAR>e : G ≃g H<GOAL>G.Preconnected ↔ H.Preconnected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>self : G.Connected<GOAL>G.Preconnected
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.Connected ↔ G.Preconnected ∧ Nonempty V
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>self : G.Connected<GOAL>Nonempty V
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.Connected ↔ ∃ v, ∀ (w : V), G.Reachable v w
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>H : SimpleGraph V'<VAR>f : G →g H<VAR>hf : Function.Surjective ⇑f<VAR>hG : G.Connected<GOAL>H.Connected
<VAR>V : Type u<VAR>G G' : SimpleGraph V<VAR>h : G ≤ G'<VAR>hG : G.Connected<GOAL>G'.Connected
<VAR>V : Type u<VAR>Nonempty V<GOAL>⊤.Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>H : SimpleGraph V'<VAR>e : G ≃g H<GOAL>G.Connected ↔ H.Connected
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Inhabited V<GOAL>default = G.connectedComponentMk default
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>β : G.ConnectedComponent → Prop<VAR>h : ∀ (v : V), β (G.connectedComponentMk v)<VAR>c : G.ConnectedComponent<GOAL>β c
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>β : G.ConnectedComponent → G.ConnectedComponent → Prop<VAR>h : ∀ (v w : V), β (G.connectedComponentMk v) (G.connectedComponentMk w)<VAR>c d : G.ConnectedComponent<GOAL>β c d
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.Reachable v w → G.connectedComponentMk v = G.connectedComponentMk w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.connectedComponentMk v = G.connectedComponentMk w → G.Reachable v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.connectedComponentMk v = G.connectedComponentMk w ↔ G.Reachable v w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>a : G.Adj v w<GOAL>G.connectedComponentMk v = G.connectedComponentMk w
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>β : Sort u_1<VAR>f : V → β<VAR>h : ∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w<VAR>v : V<GOAL>SimpleGraph.ConnectedComponent.lift f h (G.connectedComponentMk v) = f v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>p : G.ConnectedComponent → Prop<GOAL>(∃ c, p c) ↔ ∃ v, p (G.connectedComponentMk v)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>p : G.ConnectedComponent → Prop<GOAL>(∀ (c : G.ConnectedComponent), p c) ↔ ∀ (v : V), p (G.connectedComponentMk v)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>h : G.Preconnected<GOAL>Subsingleton G.ConnectedComponent
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>φ : G →g G'<VAR>v : V<GOAL>SimpleGraph.ConnectedComponent.map φ (G.connectedComponentMk v) = G'.connectedComponentMk (φ v)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>C : G.ConnectedComponent<GOAL>SimpleGraph.ConnectedComponent.map SimpleGraph.Hom.id C = C
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>C : G.ConnectedComponent<VAR>φ : G →g G'<VAR>ψ : G' →g G''<GOAL>SimpleGraph.ConnectedComponent.map ψ (SimpleGraph.ConnectedComponent.map φ C) = SimpleGraph.ConnectedComponent.map (ψ.comp φ) C
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>φ : G ≃g G'<VAR>v : V<VAR>C : G.ConnectedComponent<GOAL>G'.connectedComponentMk (φ v) = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C ↔ G.connectedComponentMk v = C
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>φ : G ≃g G'<VAR>v' : V'<VAR>C : G.ConnectedComponent<GOAL>G.connectedComponentMk (φ.symm v') = C ↔ G'.connectedComponentMk v' = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>φ : G ≃g G'<VAR>C : G'.ConnectedComponent<GOAL>φ.connectedComponentEquiv.symm C = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ.symm).toRelHom C
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>φ : G ≃g G'<VAR>C : G.ConnectedComponent<GOAL>φ.connectedComponentEquiv C = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>SimpleGraph.Iso.refl.connectedComponentEquiv = Equiv.refl G.ConnectedComponent
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>φ : G ≃g G'<GOAL>φ.symm.connectedComponentEquiv = φ.connectedComponentEquiv.symm
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>φ : G ≃g G'<VAR>φ' : G' ≃g G''<GOAL>SimpleGraph.Iso.connectedComponentEquiv (RelIso.trans φ φ') = φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>Function.Injective SimpleGraph.ConnectedComponent.supp
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>C D : G.ConnectedComponent<GOAL>C.supp = D.supp ↔ C = D
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>C : G.ConnectedComponent<VAR>v : V<GOAL>v ∈ C.supp ↔ G.connectedComponentMk v = C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v : V<GOAL>v ∈ G.connectedComponentMk v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<VAR>H : G.Subgraph<VAR>c : H.coe.ConnectedComponent<VAR>hv : v ∈ Subtype.val '' ↑c<VAR>hw : w ∈ H.verts<VAR>hadj : H.Adj v w<GOAL>w ∈ Subtype.val '' ↑c
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>Pairwise fun c c' => Disjoint c.supp c'.supp
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>⋃ c, c.supp = Set.univ
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>hconn : G.Preconnected<VAR>u v : V<GOAL>Set.univ.Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>hconn : G.Connected<VAR>u v : V<GOAL>Set.univ.Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬(G \ SimpleGraph.fromEdgeSet {s(u, v)}).Reachable u v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>(G \ SimpleGraph.fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ p, s(v, w) ∉ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>DecidableEq V<VAR>u v w : V<VAR>hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges<VAR>c : G.Walk u u<VAR>hc : c.IsTrail<VAR>he : s(v, w) ∈ c.edges<VAR>hw : w ∈ (c.takeUntil v ⋯).support<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.Adj v w ∧ (G \ SimpleGraph.fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>v w : V<GOAL>G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>e : Sym2 V<GOAL>G.IsBridge e ↔ e ∈ G.edgeSet ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>(SimpleGraph.hasse α).Adj a b ↔ a ⋖ b ∨ b ⋖ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : αᵒᵈ<GOAL>SimpleGraph.hasseDualIso a = OrderDual.ofDual a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>SimpleGraph.hasseDualIso.symm a = OrderDual.toDual a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>PartialOrder α<VAR>PartialOrder β<GOAL>SimpleGraph.hasse (α × β) = SimpleGraph.hasse α □ SimpleGraph.hasse β
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>SuccOrder α<VAR>IsSuccArchimedean α<GOAL>(SimpleGraph.hasse α).Preconnected
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>PredOrder α<VAR>IsPredArchimedean α<GOAL>(SimpleGraph.hasse α).Preconnected
<VAR>n : ℕ<VAR>u v : Fin n<GOAL>(SimpleGraph.pathGraph n).Adj u v ↔ ↑u + 1 = ↑v ∨ ↑v + 1 = ↑u
<VAR>n : ℕ<GOAL>(SimpleGraph.pathGraph n).Preconnected
<VAR>n : ℕ<GOAL>(SimpleGraph.pathGraph (n + 1)).Connected
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>(SimpleGraph.pathGraph n).chromaticNumber = 2
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>u : α<VAR>p : G.Walk u u<VAR>hOdd : Odd p.length<GOAL>3 ≤ G.chromaticNumber
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>x y : α × β<GOAL>(G □ H).Adj x y ↔ G.Adj x.1 y.1 ∧ x.2 = y.2 ∨ H.Adj x.2 y.2 ∧ x.1 = y.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>a₁ : α<VAR>b : β<VAR>a₂ : α<GOAL>(G □ H).Adj (a₁, b) (a₂, b) ↔ G.Adj a₁ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>a : α<VAR>b₁ b₂ : β<GOAL>(G □ H).Adj (a, b₁) (a, b₂) ↔ H.Adj b₁ b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>x : α × β<GOAL>(G □ H).neighborSet x = G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<GOAL>∀ (a : α × β), (G.boxProdComm H) a = a.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<GOAL>∀ (a : β × α), (RelIso.symm (G.boxProdComm H)) a = a.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>I : SimpleGraph γ<VAR>p : (α × β) × γ<GOAL>(G.boxProdAssoc H I) p = (p.1.1, p.1.2, p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>I : SimpleGraph γ<VAR>p : α × β × γ<GOAL>(RelIso.symm (G.boxProdAssoc H I)) p = ((p.1, p.2.1), p.2.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>b : β<VAR>a : α<GOAL>(G.boxProdLeft H b) a = (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>a : α<VAR>snd : β<GOAL>(G.boxProdRight H a) snd = (a, snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>DecidableEq β<VAR>DecidableRel G.Adj<VAR>a₁ a₂ : α<VAR>b : β<VAR>w : G.Walk a₁ a₂<GOAL>(SimpleGraph.Walk.boxProdLeft H b w).ofBoxProdLeft = w
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>DecidableEq α<VAR>DecidableRel G.Adj<VAR>a b₁ b₂ : α<VAR>w : G.Walk b₁ b₂<GOAL>(SimpleGraph.Walk.boxProdRight G a w).ofBoxProdRight = w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>hG : G.Preconnected<VAR>hH : H.Preconnected<GOAL>(G □ H).Preconnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>Nonempty β<VAR>h : (G □ H).Preconnected<GOAL>G.Preconnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>Nonempty α<VAR>h : (G □ H).Preconnected<GOAL>H.Preconnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>hG : G.Connected<VAR>hH : H.Connected<GOAL>(G □ H).Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>h : (G □ H).Connected<GOAL>G.Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>h : (G □ H).Connected<GOAL>H.Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<GOAL>(G □ H).Connected ↔ G.Connected ∧ H.Connected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>x : α × β<VAR>Fintype ↑(G.neighborSet x.1)<VAR>Fintype ↑(H.neighborSet x.2)<VAR>Fintype ↑((G □ H).neighborSet x)<GOAL>(G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>x : α × β<VAR>Fintype ↑(G.neighborSet x.1)<VAR>Fintype ↑(H.neighborSet x.2)<VAR>Fintype ↑((G □ H).neighborSet x)<GOAL>(G □ H).degree x = G.degree x.1 + H.degree x.2
<VAR>V : Type u_1<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>H : SimpleGraph V<VAR>hG : G.IsTuranMaximal r<VAR>hH : H.CliqueFree (r + 1)<GOAL>G ≤ H ↔ G = H
<VAR>n : ℕ<GOAL>SimpleGraph.turanGraph n 0 = ⊤
<VAR>n r : ℕ<GOAL>SimpleGraph.turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r
<VAR>n r : ℕ<VAR>hr : 0 < r<GOAL>(SimpleGraph.turanGraph n r).CliqueFree (r + 1)
<VAR>V : Type u_1<VAR>Fintype V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>hr : 0 < r<VAR>hn : r ≤ Fintype.card V<VAR>hG : G.IsTuranMaximal r<GOAL>¬G.CliqueFree r
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>r : ℕ<VAR>hr : 0 < r<GOAL>∃ H x, H.IsTuranMaximal r
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>s t : V<VAR>h : G.IsTuranMaximal r<VAR>hn : ¬G.Adj s t<GOAL>G.degree s = G.degree t
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>hts : ¬G.Adj t s<VAR>hsu : ¬G.Adj s u<GOAL>¬G.Adj t u
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>h : G.IsTuranMaximal r<GOAL>Equivalence fun x x_1 => ¬G.Adj x x_1
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>s t : V<VAR>h : G.IsTuranMaximal r<GOAL>¬G.Adj s t ↔ h.finpartition.part s = h.finpartition.part t
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>s : V<VAR>h : G.IsTuranMaximal r<GOAL>G.degree s = Fintype.card V - (h.finpartition.part s).card
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>h : G.IsTuranMaximal r<GOAL>h.finpartition.IsEquipartition
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>h : G.IsTuranMaximal r<GOAL>h.finpartition.parts.card ≤ r
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>h : G.IsTuranMaximal r<GOAL>h.finpartition.parts.card = min (Fintype.card V) r
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>h : G.IsTuranMaximal r<GOAL>Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r)
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>n r : ℕ<VAR>f : G ≃g SimpleGraph.turanGraph n r<VAR>hr : 0 < r<GOAL>G.IsTuranMaximal r
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>W : Type u_2<VAR>Fintype W<VAR>DecidableEq W<VAR>H : SimpleGraph W<VAR>DecidableRel H.Adj<VAR>h : G.IsTuranMaximal r<VAR>f : G ≃g H<VAR>hr : 0 < r<GOAL>H.IsTuranMaximal r
<VAR>n r : ℕ<VAR>hr : 0 < r<GOAL>(SimpleGraph.turanGraph n r).IsTuranMaximal r
<VAR>V : Type u_1<VAR>Fintype V<VAR>DecidableEq V<VAR>G : SimpleGraph V<VAR>DecidableRel G.Adj<VAR>r : ℕ<VAR>hr : 0 < r<GOAL>G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>DecidableEq V<VAR>v : V<GOAL>Finset.filter (fun d => d.toProd.1 = v) Finset.univ = Finset.image (G.dartOfNeighborSet v) Finset.univ
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>DecidableEq V<VAR>v : V<GOAL>(Finset.filter (fun d => d.toProd.1 = v) Finset.univ).card = G.degree v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<GOAL>Fintype.card G.Dart = ∑ v : V, G.degree v
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>DecidableEq V<VAR>d : G.Dart<GOAL>Finset.filter (fun d' => d'.edge = d.edge) Finset.univ = {d, d.symm}
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>DecidableEq V<VAR>e : Sym2 V<VAR>h : e ∈ G.edgeSet<GOAL>(Finset.filter (fun d => d.edge = e) Finset.univ).card = 2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>Fintype (Sym2 V)<GOAL>Fintype.card G.Dart = 2 * G.edgeFinset.card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>Fintype (Sym2 V)<GOAL>∑ v : V, G.degree v = 2 * G.edgeFinset.card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>Fintype (Sym2 V)<GOAL>2 * G.edgeFinset.card = (Finset.filter (fun x => match x with | (x, y) => G.Adj x y) Finset.univ).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<GOAL>Even (Finset.filter (fun v => Odd (G.degree v)) Finset.univ).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableEq V<VAR>DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<GOAL>Odd (Finset.filter (fun w => w ≠ v ∧ Odd (G.degree w)) Finset.univ).card
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>DecidableRel G.Adj<VAR>v : V<VAR>h : Odd (G.degree v)<GOAL>∃ w, w ≠ v ∧ Odd (G.degree w)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.edist u v = sInf (Set.range fun w => ↑w.length)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>hr : G.Reachable u v<GOAL>∃ p, ↑p.length = G.edist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>hconn : G.Connected<VAR>u v : V<GOAL>∃ p, ↑p.length = G.edist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>G.edist u v ≤ ↑p.length
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.edist u v = 0 ↔ u = v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>v : V<GOAL>G.edist v v = 0
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>hne : u ≠ v<GOAL>0 < G.edist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : ¬G.Reachable u v<GOAL>G.edist u v = ⊤
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.edist u v ≠ ⊤<GOAL>G.Reachable u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>h : G.edist u v ≠ ⊤<GOAL>∃ p, ↑p.length = G.edist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.edist u v = G.edist v u
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>k : ℕ<VAR>h : G.edist u v = ↑k<GOAL>∃ p, p.length = k
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.edist u v ≠ ⊤ ↔ G.Reachable u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.edist u v = 1 ↔ G.Adj u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.dist u v = sInf (Set.range SimpleGraph.Walk.length)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>hr : G.Reachable u v<GOAL>∃ p, p.length = G.dist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>hconn : G.Connected<VAR>u v : V<GOAL>∃ p, p.length = G.dist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<VAR>p : G.Walk u v<GOAL>G.dist u v ≤ p.length
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v : V<GOAL>G.dist u v = 0 ↔ u = v ∨ ¬G.Reachable u v