ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>G : SimpleGraph V<GOAL>G.IsTree ↔ Nonempty V ∧ ∀ (v w : V), ∃! p, p.IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>hG : G.IsTree<VAR>v w : V<GOAL>∃! p, p.IsPath
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>Fintype V<VAR>Fintype ↑G.edgeSet<VAR>hG : G.IsTree<GOAL>G.edgeFinset.card + 1 = Fintype.card V
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>m a b : ℕ<VAR>P : Finpartition s<VAR>hs : a * m + b * (m + 1) = s.card<GOAL>∃ Q, (∀ x ∈ Q.parts, x.card = m ∨ x.card = m + 1) ∧ (∀ x ∈ P.parts, (x \ (Finset.filter (fun y => y ⊆ x) Q.parts).biUnion id).card ≤ m) ∧ (Finset.filter (fun i => i.card = m + 1) Q.parts).card = b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>m a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<GOAL>t ∈ (Finpartition.equitabilise h).parts → t.card = m ∨ t.card = m + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>m a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<GOAL>(Finpartition.equitabilise h).IsEquipartition
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>m a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<GOAL>(Finset.filter (fun u => u.card = m + 1) (Finpartition.equitabilise h).parts).card = b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>m a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<GOAL>(Finset.filter (fun u => u.card = m) (Finpartition.equitabilise h).parts).card = a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>m a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<VAR>hm : m ≠ 0<GOAL>(Finpartition.equitabilise h).parts.card = a + b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>m a b : ℕ<VAR>P : Finpartition s<VAR>h : a * m + b * (m + 1) = s.card<GOAL>t ∈ P.parts → (t \ (Finset.filter (fun u => u ⊆ t) (Finpartition.equitabilise h).parts).biUnion id).card ≤ m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hs : n ≤ s.card<GOAL>∃ P, P.IsEquipartition ∧ P.parts.card = n
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t : Finset β<VAR>x : α × β<GOAL>x ∈ Rel.interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b : β<GOAL>(a, b) ∈ Rel.interedges r s t ↔ a ∈ s ∧ b ∈ t ∧ r a b
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>t : Finset β<GOAL>Rel.interedges r ∅ t = ∅
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<GOAL>Rel.interedges r s₂ t₂ ⊆ Rel.interedges r s₁ t₁
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t : Finset β<GOAL>(Rel.interedges r s t).card + (Rel.interedges (fun x y => ¬r x y) s t).card = s.card * t.card
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s s' : Finset α<VAR>hs : Disjoint s s'<VAR>t : Finset β<GOAL>Disjoint (Rel.interedges r s t) (Rel.interedges r s' t)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t t' : Finset β<VAR>ht : Disjoint t t'<GOAL>Disjoint (Rel.interedges r s t) (Rel.interedges r s t')
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t : Finset β<VAR>DecidableEq α<VAR>DecidableEq β<GOAL>Rel.interedges r s t = s.biUnion fun x => Finset.map { toFun := fun x_1 => (x, x_1), inj' := ⋯ } (Finset.filter (r x) t)
<VAR>ι : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Finset ι<VAR>t : Finset β<VAR>f : ι → Finset α<GOAL>Rel.interedges r (s.biUnion f) t = s.biUnion fun a => Rel.interedges r (f a) t
<VAR>ι : Type u_2<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset ι<VAR>f : ι → Finset β<GOAL>Rel.interedges r s (t.biUnion f) = t.biUnion fun b => Rel.interedges r s (f b)
<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>DecidableEq α<VAR>DecidableEq β<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → Finset α<VAR>g : κ → Finset β<GOAL>Rel.interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab => Rel.interedges r (f ab.1) (g ab.2)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t : Finset β<GOAL>(Rel.interedges r s t).card ≤ s.card * t.card
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t : Finset β<GOAL>0 ≤ Rel.edgeDensity r s t
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t : Finset β<GOAL>Rel.edgeDensity r s t ≤ 1
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t : Finset β<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>Rel.edgeDensity r s t + Rel.edgeDensity (fun x y => ¬r x y) s t = 1
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>t : Finset β<GOAL>Rel.edgeDensity r ∅ t = 0
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<GOAL>Rel.edgeDensity r s ∅ = 0
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>DecidableEq α<VAR>P : Finpartition s<VAR>t : Finset β<GOAL>(Rel.interedges r s t).card = ∑ a ∈ P.parts, (Rel.interedges r a t).card
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>t : Finset β<VAR>DecidableEq β<VAR>s : Finset α<VAR>P : Finpartition t<GOAL>(Rel.interedges r s t).card = ∑ b ∈ P.parts, (Rel.interedges r s b).card
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s : Finset α<VAR>t : Finset β<VAR>DecidableEq α<VAR>DecidableEq β<VAR>P : Finpartition s<VAR>Q : Finpartition t<GOAL>(Rel.interedges r s t).card = ∑ ab ∈ P.parts ×ˢ Q.parts, (Rel.interedges r ab.1 ab.2).card
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) * Rel.edgeDensity r s₂ t₂ ≤ Rel.edgeDensity r s₁ t₁
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁ ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hs₂ : s₂.Nonempty<VAR>ht₂ : t₂.Nonempty<GOAL>|Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁| ≤ 1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)
<VAR>𝕜 : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : δ < 1<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<GOAL>|↑(Rel.edgeDensity r s₂ t₂) - ↑(Rel.edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
<VAR>𝕜 : Type u_1<VAR>α : Type u_4<VAR>β : Type u_5<VAR>LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>(a : α) → DecidablePred (r a)<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ : 0 ≤ δ<VAR>hscard : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>htcard : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<GOAL>|↑(Rel.edgeDensity r s₂ t₂) - ↑(Rel.edgeDensity r s₁ t₁)| ≤ 2 * δ
<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>s t : Finset α<VAR>hr : Symmetric r<VAR>x : α × α<GOAL>x.swap ∈ Rel.interedges r s t ↔ x ∈ Rel.interedges r t s
<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>s t : Finset α<VAR>a b : α<VAR>hr : Symmetric r<GOAL>(a, b) ∈ Rel.interedges r s t ↔ (b, a) ∈ Rel.interedges r t s
<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>hr : Symmetric r<VAR>s t : Finset α<GOAL>(Rel.interedges r s t).card = (Rel.interedges r t s).card
<VAR>α : Type u_4<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>hr : Symmetric r<VAR>s t : Finset α<GOAL>Rel.edgeDensity r s t = Rel.edgeDensity r t s
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<GOAL>G.interedges s t = Finset.filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<GOAL>G.edgeDensity s t = ↑(G.interedges s t).card / (↑s.card * ↑t.card)
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<GOAL>↑(G.interedges s t).card / (↑s.card * ↑t.card) = G.edgeDensity s t
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<VAR>x : α × α<GOAL>x ∈ G.interedges s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ G.Adj x.1 x.2
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<VAR>a b : α<GOAL>(a, b) ∈ G.interedges s t ↔ a ∈ s ∧ b ∈ t ∧ G.Adj a b
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>t : Finset α<GOAL>G.interedges ∅ t = ∅
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₂ ⊆ s₁ → t₂ ⊆ t₁ → G.interedges s₂ t₂ ⊆ G.interedges s₁ t₁
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s₁ s₂ : Finset α<VAR>hs : Disjoint s₁ s₂<VAR>t : Finset α<GOAL>Disjoint (G.interedges s₁ t) (G.interedges s₂ t)
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>t₁ t₂ : Finset α<VAR>s : Finset α<VAR>ht : Disjoint t₁ t₂<GOAL>Disjoint (G.interedges s t₁) (G.interedges s t₂)
<VAR>ι : Type u_2<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>DecidableEq α<VAR>s : Finset ι<VAR>t : Finset α<VAR>f : ι → Finset α<GOAL>G.interedges (s.biUnion f) t = s.biUnion fun a => G.interedges (f a) t
<VAR>ι : Type u_2<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>DecidableEq α<VAR>s : Finset α<VAR>t : Finset ι<VAR>f : ι → Finset α<GOAL>G.interedges s (t.biUnion f) = t.biUnion fun b => G.interedges s (f b)
<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>DecidableEq α<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → Finset α<VAR>g : κ → Finset α<GOAL>G.interedges (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab => G.interedges (f ab.1) (g ab.2)
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<VAR>DecidableEq α<VAR>h : Disjoint s t<GOAL>(G.interedges s t).card + (Gᶜ.interedges s t).card = s.card * t.card
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<VAR>DecidableEq α<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<VAR>h : Disjoint s t<GOAL>G.edgeDensity s t + Gᶜ.edgeDensity s t = 1
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<GOAL>(G.interedges s t).card ≤ s.card * t.card
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<GOAL>0 ≤ G.edgeDensity s t
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<GOAL>G.edgeDensity s t ≤ 1
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>t : Finset α<GOAL>G.edgeDensity ∅ t = 0
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s : Finset α<GOAL>G.edgeDensity s ∅ = 0
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<VAR>x : α × α<GOAL>x.swap ∈ G.interedges s t ↔ x ∈ G.interedges t s
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<VAR>a b : α<GOAL>(a, b) ∈ G.interedges s t ↔ (b, a) ∈ G.interedges t s
<VAR>α : Type u_4<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<GOAL>G.edgeDensity s t = G.edgeDensity t s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>ε' : 𝕜<VAR>h : ε ≤ ε'<VAR>hε : G.IsUniform ε s t<GOAL>G.IsUniform ε' s t
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<GOAL>Symmetric (G.IsUniform ε)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<GOAL>G.IsUniform ε s t ↔ G.IsUniform ε t s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<GOAL>G.IsUniform 1 s t
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>hG : G.IsUniform ε s t<GOAL>0 < ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>a b : α<GOAL>G.IsUniform ε {a} {b} ↔ 0 < ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>s t : Finset α<GOAL>¬G.IsUniform 0 s t
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<GOAL>¬G.IsUniform ε s t ↔ ∃ s' ⊆ s, ∃ t' ⊆ t, ↑s.card * ε ≤ ↑s'.card ∧ ↑t.card * ε ≤ ↑t'.card ∧ ε ≤ ↑|G.edgeDensity s' t' - G.edgeDensity s t|
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>h : ¬G.IsUniform ε s t<GOAL>(G.nonuniformWitnesses ε s t).1 ⊆ s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>h : ¬G.IsUniform ε s t<GOAL>↑s.card * ε ≤ ↑(G.nonuniformWitnesses ε s t).1.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>h : ¬G.IsUniform ε s t<GOAL>(G.nonuniformWitnesses ε s t).2 ⊆ t
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>h : ¬G.IsUniform ε s t<GOAL>↑t.card * ε ≤ ↑(G.nonuniformWitnesses ε s t).2.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>h : ¬G.IsUniform ε s t<GOAL>ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>h : ¬G.IsUniform ε s t<GOAL>G.nonuniformWitness ε s t ⊆ s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>h : ¬G.IsUniform ε s t<GOAL>↑s.card * ε ≤ ↑(G.nonuniformWitness ε s t).card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>h₁ : s ≠ t<VAR>h₂ : ¬G.IsUniform ε s t<GOAL>ε ≤ ↑|G.edgeDensity (G.nonuniformWitness ε s t) (G.nonuniformWitness ε t s) - G.edgeDensity s t|
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>u v : Finset α<VAR>ε : 𝕜<GOAL>(u, v) ∈ P.sparsePairs G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ↑(G.edgeDensity u v) < ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε ε' : 𝕜<VAR>h : ε ≤ ε'<GOAL>P.sparsePairs G ε ⊆ P.sparsePairs G ε'
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>u v : Finset α<GOAL>(u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε ε' : 𝕜<VAR>h : ε ≤ ε'<GOAL>P.nonUniforms G ε' ⊆ P.nonUniforms G ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>hε : 0 < ε<GOAL>⊥.nonUniforms G ε = ∅
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>hε : 0 < ε<GOAL>⊥.IsUniform G ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<GOAL>P.IsUniform G 1
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε ε' : 𝕜<VAR>hP : P.IsUniform G ε<VAR>h : ε ≤ ε'<GOAL>P.IsUniform G ε'
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>hP : P.parts = ∅<GOAL>P.IsUniform G ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>h : ¬P.IsUniform G ε<GOAL>P.parts.Nonempty
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>h : ¬G.IsUniform ε s t<VAR>ht : t ∈ P.parts<VAR>hst : s ≠ t<GOAL>G.nonuniformWitness ε s t ∈ P.nonuniformWitnesses G ε s
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>hP : P.IsEquipartition<VAR>hε : 0 ≤ ε<GOAL>↑((P.sparsePairs G ε).biUnion fun x => match x with | (U, V) => G.interedges U V).card ≤ ε * (↑A.card + ↑P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>hP : P.IsEquipartition<VAR>hε : 0 ≤ ε<GOAL>↑((P.sparsePairs G ε).biUnion fun x => match x with | (U, V) => G.interedges U V).card ≤ 4 * ε * ↑A.card ^ 2
<VAR>i j : ℕ<VAR>hj : 0 < j<GOAL>j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>hP : P.IsEquipartition<GOAL>↑(P.parts.biUnion Finset.offDiag).card ≤ ↑A.card * (↑A.card + ↑P.parts.card) / ↑P.parts.card
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>ε : 𝕜<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hP' : 4 / ε ≤ ↑P.parts.card<GOAL>↑(P.parts.biUnion Finset.offDiag).card ≤ ε / 2 * ↑A.card ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>hA : A.Nonempty<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hG : P.IsUniform G ε<GOAL>∑ i ∈ P.nonUniforms G ε, ↑i.1.card * ↑i.2.card < ε * (↑A.card + ↑P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<VAR>hA : A.Nonempty<VAR>hε : 0 < ε<VAR>hP : P.IsEquipartition<VAR>hG : P.IsUniform G ε<GOAL>↑((P.nonUniforms G ε).biUnion fun x => match x with | (U, V) => U ×ˢ V).card < 4 * ε * ↑A.card ^ 2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>a b : α<GOAL>(SimpleGraph.regularityReduced P G ε δ).Adj a b = (G.Adj a b ∧ ∃ U ∈ P.parts, ∃ V ∈ P.parts, a ∈ U ∧ b ∈ V ∧ U ≠ V ∧ G.IsUniform ε U V ∧ δ ≤ ↑(G.edgeDensity U V))
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε δ : 𝕜<GOAL>SimpleGraph.regularityReduced P G ε δ ≤ G
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>δ ε₁ ε₂ : 𝕜<VAR>hε : ε₁ ≤ ε₂<GOAL>SimpleGraph.regularityReduced P G ε₁ δ ≤ SimpleGraph.regularityReduced P G ε₂ δ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε δ₁ δ₂ : 𝕜<VAR>hδ : δ₁ ≤ δ₂<GOAL>SimpleGraph.regularityReduced P G ε δ₂ ≤ SimpleGraph.regularityReduced P G ε δ₁
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>LinearOrderedField 𝕜<VAR>DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>DecidableRel G.Adj<VAR>ε : 𝕜<GOAL>Finset.filter (fun x => match x with | (x, y) => G.Adj x y ∧ ¬(SimpleGraph.regularityReduced P G (ε / 8) (ε / 4)).Adj x y) (A ×ˢ A) ⊆ ((P.nonUniforms G (ε / 8)).biUnion fun x => match x with | (U, V) => U ×ˢ V) ∪ P.parts.biUnion Finset.offDiag ∪ (P.sparsePairs G (ε / 4)).biUnion fun x => match x with | (U, V) => G.interedges U V
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<GOAL>Function.Injective SimpleGraph.ComponentCompl.supp
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>C D : G.ComponentCompl K<GOAL>C.supp = D.supp ↔ C = D
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>v : V<VAR>C : G.ComponentCompl K<GOAL>v ∈ C ↔ ∃ (vK : v ∉ K), G.componentComplMk vK = C
<VAR>V : Type u<VAR>K : Set V<VAR>G : SimpleGraph V<VAR>v : V<VAR>vK : v ∉ K<GOAL>v ∈ G.componentComplMk vK
<VAR>V : Type u<VAR>K : Set V<VAR>G : SimpleGraph V<VAR>v w : V<VAR>vK : v ∉ K<VAR>wK : w ∉ K<VAR>a : G.Adj v w<GOAL>G.componentComplMk vK = G.componentComplMk wK
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>β : G.ComponentCompl K → Prop<VAR>f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)<VAR>C : G.ComponentCompl K<GOAL>β C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>C D : G.ComponentCompl K<GOAL>↑C = ↑D ↔ C = D
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>C : G.ComponentCompl K<GOAL>(↑C).Nonempty
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>C : G.ComponentCompl K<GOAL>∃ v, ∃ (h : v ∉ K), G.componentComplMk h = C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>C : G.ComponentCompl K<GOAL>Disjoint K ↑C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>C : G.ComponentCompl K<VAR>c : V<VAR>cC : c ∈ C<GOAL>c ∉ K
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<GOAL>Pairwise fun C D => Disjoint ↑C ↑D
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>C : G.ComponentCompl K<VAR>c d : V<GOAL>c ∈ C → d ∉ K → G.Adj c d → d ∈ C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K : Set V<VAR>Gc : G.Preconnected<VAR>hK : K.Nonempty<VAR>C : G.ComponentCompl K<GOAL>∃ ck, ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L : Set V<VAR>C : G.ComponentCompl L<VAR>h : K ⊆ L<GOAL>↑C ⊆ ↑(SimpleGraph.ComponentCompl.hom h C)
<VAR>V : Type u<VAR>K L : Set V<VAR>G : SimpleGraph V<VAR>v : V<VAR>vK : v ∉ K<VAR>h : L ⊆ K<GOAL>v ∈ SimpleGraph.ComponentCompl.hom h (G.componentComplMk vK)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L : Set V<VAR>C : G.ComponentCompl L<VAR>h : K ⊆ L<VAR>D : G.ComponentCompl K<GOAL>SimpleGraph.ComponentCompl.hom h C = D ↔ ↑C ⊆ ↑D
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L : Set V<VAR>C : G.ComponentCompl L<VAR>h : K ⊆ L<VAR>D : G.ComponentCompl K<GOAL>SimpleGraph.ComponentCompl.hom h C = D ↔ ¬Disjoint ↑C ↑D
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>L : Set V<VAR>C : G.ComponentCompl L<GOAL>SimpleGraph.ComponentCompl.hom ⋯ C = C