ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hGε : ↑(G.edgeDensity U V) ≤ ε ^ 5 / 50<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hGε : ε ^ 5 / 50 ≤ ↑(G.edgeDensity U V)<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50<VAR>this : ↑(G.edgeDensity U V) - ε ^ 5 / 50 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤ ((∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card) ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50<VAR>this : ↑(G.edgeDensity U V) - ε ^ 5 / 50 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card<GOAL>↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤ (↑(G.edgeDensity U V) - ε ^ 5 / 50) ^ 2
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50<VAR>this : ↑(G.edgeDensity U V) - ε ^ 5 / 50 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card<GOAL>2 * ↑(G.edgeDensity U V) * (ε ^ 5 / 50) - (ε ^ 5 / 50) ^ 2 ≤ ε ^ 5 / 25
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50<VAR>this : ↑(G.edgeDensity U V) - ε ^ 5 / 50 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card<GOAL>2 * ↑(G.edgeDensity U V) * (ε ^ 5 / 50) ≤ ε ^ 5 / 25
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU✝ : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hU : U ∈ P.parts<VAR>hV : V ∈ P.parts<VAR>hGε : 0 ≤ ↑(G.edgeDensity U V) - ε ^ 5 / 50<VAR>this : ↑(G.edgeDensity U V) - ε ^ 5 / 50 ≤ (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2)) / 16 ^ P.parts.card<GOAL>ε ^ 5 * 25⁻¹ * ↑(G.edgeDensity U V) ≤ ε ^ 5 * 25⁻¹
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<GOAL>(inducedMap A).fst = univ
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<GOAL>∀ (x : ℕ → β), x ∈ (inducedMap A).fst
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<VAR>x : ℕ → β<VAR>u : ℕ → α<VAR>hu : ∀ (n : ℕ), u n ∈ A (res x n)<GOAL>x ∈ (inducedMap A).fst
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<VAR>x : ℕ → β<VAR>u : ℕ → α<VAR>hu : ∀ (n : ℕ), u n ∈ A (res x n)<VAR>umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)<GOAL>x ∈ (inducedMap A).fst
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<VAR>x : ℕ → β<VAR>u : ℕ → α<VAR>hu : ∀ (n : ℕ), u n ∈ A (res x n)<VAR>umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)<VAR>this : CauchySeq u<GOAL>x ∈ (inducedMap A).fst
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<VAR>x : ℕ → β<VAR>u : ℕ → α<VAR>hu : ∀ (n : ℕ), u n ∈ A (res x n)<VAR>umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)<VAR>this : CauchySeq u<VAR>y : α<VAR>hy : Tendsto u atTop (𝓝 y)<GOAL>x ∈ (inducedMap A).fst
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<VAR>x : ℕ → β<VAR>u : ℕ → α<VAR>hu : ∀ (n : ℕ), u n ∈ A (res x n)<VAR>umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)<VAR>this : CauchySeq u<VAR>y : α<VAR>hy : Tendsto u atTop (𝓝 y)<GOAL>y ∈ ⋂ n, A (res x n)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<VAR>x : ℕ → β<VAR>u : ℕ → α<VAR>hu : ∀ (n : ℕ), u n ∈ A (res x n)<VAR>umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)<VAR>this : CauchySeq u<VAR>y : α<VAR>hy : Tendsto u atTop (𝓝 y)<GOAL>∀ (i : ℕ), y ∈ A (res x i)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<VAR>x : ℕ → β<VAR>u : ℕ → α<VAR>hu : ∀ (n : ℕ), u n ∈ A (res x n)<VAR>umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)<VAR>this : CauchySeq u<VAR>y : α<VAR>hy : Tendsto u atTop (𝓝 y)<VAR>n : ℕ<GOAL>y ∈ closure (A (x n :: res x n))
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<VAR>x : ℕ → β<VAR>u : ℕ → α<VAR>hu : ∀ (n : ℕ), u n ∈ A (res x n)<VAR>umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)<VAR>this : CauchySeq u<VAR>y : α<VAR>hy : Tendsto u atTop (𝓝 y)<VAR>n : ℕ<GOAL>∀ᶠ (x_1 : ℕ) in atTop, u x_1 ∈ A (x n :: res x n)
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>A : List β → Set α<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : CompleteSpace α<VAR>hdiam : VanishingDiam A<VAR>hanti : ClosureAntitone A<VAR>hnonempty : ∀ (l : List β), (A l).Nonempty<VAR>x : ℕ → β<VAR>u : ℕ → α<VAR>hu : ∀ (n : ℕ), u n ∈ A (res x n)<VAR>umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)<VAR>this : CauchySeq u<VAR>y : α<VAR>hy : Tendsto u atTop (𝓝 y)<VAR>n : ℕ<GOAL>∃ a, ∀ b ≥ a, u b ∈ A (x n :: res x n)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁶ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝³ : FunLike F M M₂<VAR>inst✝² : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>M' : Type u_9<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>q₁ q₁' : Submodule R M'<VAR>x : M<VAR>y : M'<GOAL>(x, y) ∈ ⊥.prod ⊥ ↔ (x, y) ∈ ⊥
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Mul α<VAR>x : α<VAR>v : Fin n → α<VAR>w : Fin n.succ → α<GOAL>vecCons x v ⬝ᵥ w = x * vecHead w + v ⬝ᵥ vecTail w
<VAR>R : Type u<VAR>inst✝⁴ : NonUnitalSemiring R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : Nontrivial R<VAR>x : R<VAR>hx : IsRegular x<GOAL>0 < star x * x
<VAR>R : Type u<VAR>inst✝⁴ : NonUnitalSemiring R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : Nontrivial R<VAR>x : R<VAR>hx : IsRegular x<GOAL>0 ≠ x
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : t ⊆ s<VAR>x : α<GOAL>x ∈ val '' {x | ↑x ∈ t} ↔ x ∈ t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : t ⊆ s<VAR>x : α<GOAL>(∃ x_1 ∈ {x | ↑x ∈ t}, ↑x_1 = x) ↔ x ∈ t
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : TopologicalSpace Y<VAR>f : Filter X✝<VAR>s t s₁ s₂ t₁ t₂ : Set X✝<VAR>x : X✝<VAR>X : Type u_3<VAR>inst✝ : TopologicalSpace (X × X)<GOAL>𝓝ˢ (diagonal X) = ⨆ x, 𝓝 (x, x)
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : TopologicalSpace Y<VAR>f : Filter X✝<VAR>s t s₁ s₂ t₁ t₂ : Set X✝<VAR>x : X✝<VAR>X : Type u_3<VAR>inst✝ : TopologicalSpace (X × X)<GOAL>sSup (range (𝓝 ∘ fun x => (x, x))) = ⨆ x, 𝓝 (x, x)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<GOAL>IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : ContinuousAdd E<VAR>t : Set E<GOAL>IsVonNBounded 𝕜 (∅ + t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 ∅ ∧ IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : s.Nonempty<GOAL>IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : ContinuousAdd E<VAR>s : Set E<VAR>hs : s.Nonempty<GOAL>IsVonNBounded 𝕜 (s + ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 ∅
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁✝ l₂✝ : List α<VAR>a : α<VAR>f : α → β → β<VAR>l₁ l₂ : List α<VAR>lcomm : LeftCommutative f<VAR>p : l₁ ~ l₂<VAR>b : β<GOAL>foldr f b l₁ = foldr f b l₂
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>ι' : Sort u_1<VAR>inst✝ : Inv G<VAR>ts' : ι' → TopologicalSpace G<VAR>h' : ∀ (i : ι'), ContinuousInv G<GOAL>ContinuousInv G
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁✝ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a✝ b a : α<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ a :: l₂).Nodup ↔ (a :: (l₁ ++ l₂)).Nodup
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>ζ : (𝓞 K)ˣ<GOAL>ζ ∈ rootsOfUnity (torsionOrder K) (𝓞 K) ↔ ζ ∈ torsion K
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>ζ : (𝓞 K)ˣ<GOAL>ζ ^ ↑(torsionOrder K) = 1 ↔ ζ ∈ CommGroup.torsion (𝓞 K)ˣ
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>C : Type u_6<VAR>inst✝ : CommGroup C<VAR>s t : Subgroup C<VAR>x : C<GOAL>(∃ y ∈ s, ∃ z ∈ t, y * z = x) ↔ ∃ y z, ↑y * ↑z = x
<VAR>r : ℝ<GOAL>r.toNNReal ≤ 1 ↔ r ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x : S<GOAL>h.map (h.modByMonicHom x) = x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x : S<GOAL>h.map ({ toFun := fun x => h.repr x %ₘ f, map_add' := ⋯ } x) = x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x : S<GOAL>h.map (h.repr x %ₘ f) = x
<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>u v : V<VAR>p : G.Walk u v<GOAL>p.reverse.darts = (List.map Dart.symm p.darts).reverse
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℕ → M<VAR>k : ℕ<VAR>h : HasProd (fun n => f (n + k)) m<GOAL>HasProd f ((∏ i ∈ range k, f i) * m)
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝¹ : CommGroup G<VAR>g g' : G<VAR>inst✝ : ContinuousMul M<VAR>f : ℕ → M<VAR>k : ℕ<VAR>h : HasProd (fun n => f (n + k)) m<GOAL>HasProd (f ∘ Subtype.val) m
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝ : RingHomSurjective τ₂₁<VAR>p : Submodule R M<VAR>f : M₂ →ₛₗ[τ₂₁] M<VAR>hf : ∀ (c : M₂), f c ∈ p<GOAL>range (codRestrict p f hf) = comap p.subtype (range f)
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f : R[X]<VAR>n : ℕ<VAR>h : (f ^ (n + 2)).Separable<GOAL>IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>f : R[X]<VAR>n : ℕ<VAR>h : (f ^ n * f * f).Separable<GOAL>IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0
<VAR>a b c d m n : ℤ<VAR>hb : 0 < b<GOAL>0 ≤ a * b ↔ 0 ≤ a
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : IsPreconnected J<VAR>p : Set J<VAR>j₀ : J<VAR>h0 : j₀ ∈ p<VAR>h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)<VAR>j : J<GOAL>j ∈ p
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : IsPreconnected J<VAR>p : Set J<VAR>j₀ : J<VAR>h0 : j₀ ∈ p<VAR>h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)<VAR>j : J<VAR>aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } := fun j₁ j₂ f => congrArg ULift.up (Iff.eq (h1 f))<GOAL>j ∈ p
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : IsPreconnected J<VAR>p : Set J<VAR>j₀ : J<VAR>h0 : j₀ ∈ p<VAR>h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)<VAR>j : J<VAR>aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } := fun j₁ j₂ f => congrArg ULift.up (Iff.eq (h1 f))<VAR>i : (j ∈ p) = (j₀ ∈ p)<GOAL>j ∈ p
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp✝ : Fact (1 ≤ p)<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>hp : p ≠ ⊤<VAR>x y : WithLp p (α × β)<GOAL>dist x y = (dist x.1 y.1 ^ p.toReal + dist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h✝ : x ∈ l<VAR>y : α<VAR>h : x ∈ y :: l<VAR>hy : x ≠ y<VAR>hx : x ≠ (y :: l).getLast ⋯<GOAL>(y :: l).next x h = l.next x ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h✝ : x ∈ l<VAR>y : α<VAR>h : x ∈ y :: l<VAR>hy : x ≠ y<VAR>hx : x ≠ (y :: l).getLast ⋯<GOAL>x ∈ l
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x : α<VAR>h✝ : x ∈ l<VAR>y : α<VAR>h : x ∈ y :: l<VAR>hy : x ≠ y<VAR>hx : x ≠ (y :: l).getLast ⋯<GOAL>x ≠ l.getLast ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y ≠ -y - W.a₁ * x - W.a₃)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<GOAL>W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0) ↔ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y - (-y - W.a₁ * x - W.a₃) ≠ 0)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : ConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : 0 < ∑ i ∈ t, w i<VAR>hmem : ∀ i ∈ t, p i ∈ s<GOAL>f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : ConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 ≤ w i<VAR>h₁ : 0 < ∑ i ∈ t, w i<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p | p.1 ∈ s ∧ f p.1 ≤ p.2}<GOAL>f (t.centerMass w p) ≤ t.centerMass w (f ∘ p)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P : R[X]<VAR>this : ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i<GOAL>IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : CommRing R<VAR>P : R[X]<VAR>this : ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i<GOAL>(IsUnit ((C r + X * P).coeff 0) ∧ ∀ (i : ℕ), IsNilpotent (P.coeff i)) ↔ IsUnit r ∧ IsNilpotent P
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y z w : ℤ<VAR>h1 : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0<VAR>h2 : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0<GOAL>{ re := x, im := y } = 0 ∨ { re := z, im := w } = 0
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y z w : ℤ<VAR>h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0<VAR>h2 : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0<VAR>h1 : x * z = -(↑d * y * w)<GOAL>{ re := x, im := y } = 0 ∨ { re := z, im := w } = 0
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y z w : ℤ<VAR>h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0<VAR>h2✝ : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0<VAR>h1 : x * z = -(↑d * y * w)<VAR>h2 : x * w = -(y * z)<GOAL>{ re := x, im := y } = 0 ∨ { re := z, im := w } = 0
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>x y z w : ℤ<VAR>h1✝ : { re := x, im := y }.re * { re := z, im := w }.re + ↑d * { re := x, im := y }.im * { re := z, im := w }.im = 0<VAR>h2✝ : { re := x, im := y }.re * { re := z, im := w }.im + { re := x, im := y }.im * { re := z, im := w }.re = 0<VAR>h1 : x * z = -(↑d * y * w)<VAR>h2 : x * w = -(y * z)<VAR>fin : x * x = ↑d * y * y → { re := x, im := y } = 0<GOAL>{ re := x, im := y } = 0 ∨ { re := z, im := w } = 0
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>𝕝 : Type u_3<VAR>R : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>M : Type u_7<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : CommSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommMonoid F<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>l : Filter α<VAR>f : α → WeakBilin B<VAR>x : WeakBilin B<VAR>hB : Function.Injective ⇑B<GOAL>Tendsto f l (𝓝 x) ↔ ∀ (y : F), Tendsto (fun i => (B (f i)) y) l (𝓝 ((B x) y))
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>𝕝 : Type u_3<VAR>R : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>M : Type u_7<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : CommSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommMonoid F<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>l : Filter α<VAR>f : α → WeakBilin B<VAR>x : WeakBilin B<VAR>hB : Function.Injective ⇑B<GOAL>Tendsto ((fun x y => (B x) y) ∘ f) l (𝓝 fun y => (B x) y) ↔ Tendsto (fun i => ⇑(B (f i))) l (𝓝 ⇑(B x))
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PredOrder α<VAR>inst✝ : SuccOrder α<GOAL>⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}