ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>f : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Inducing f<VAR>s : Set α<VAR>hs : IsSeparable s<VAR>this✝¹ : SeparableSpace ↑s<VAR>this✝ : SecondCountableTopology ↑s<VAR>this : Inducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)<GOAL>IsSeparable (f ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s✝ : Set α<VAR>f : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Inducing f<VAR>s : Set α<VAR>hs : IsSeparable s<VAR>this✝² : SeparableSpace ↑s<VAR>this✝¹ : SecondCountableTopology ↑s<VAR>this✝ : Inducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)<VAR>this : SecondCountableTopology ↑(f ⁻¹' s)<GOAL>IsSeparable (f ⁻¹' s)
<VAR>a b p q : ℝ≥0<VAR>h : p.IsConjExponent q<GOAL>p⁻¹ + q⁻¹ = 1
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{?u.23801, u_1} D<VAR>P : MorphismProperty C<VAR>inst✝ : P.RespectsIso<GOAL>P.map (𝟭 C) = P
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = ⊤<VAR>x : α<VAR>H : Subgroup (Perm α) := closure {σ, swap x (σ x)}<GOAL>closure {σ, swap x (σ x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = ⊤<VAR>x : α<VAR>H : Subgroup (Perm α) := closure {σ, swap x (σ x)}<VAR>h3 : σ ∈ H<GOAL>closure {σ, swap x (σ x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = ⊤<VAR>x : α<VAR>H : Subgroup (Perm α) := closure {σ, swap x (σ x)}<VAR>h3 : σ ∈ H<VAR>h4 : swap x (σ x) ∈ H<GOAL>closure {σ, swap x (σ x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = ⊤<VAR>x : α<VAR>H : Subgroup (Perm α) := closure {σ, swap x (σ x)}<VAR>h3 : σ ∈ H<VAR>h4 : swap x (σ x) ∈ H<VAR>step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H<VAR>step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H<GOAL>closure {σ, swap x (σ x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = ⊤<VAR>x : α<VAR>H : Subgroup (Perm α) := closure {σ, swap x (σ x)}<VAR>h3 : σ ∈ H<VAR>h4 : swap x (σ x) ∈ H<VAR>step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H<VAR>step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H<VAR>step3 : ∀ (y : α), swap x y ∈ H<GOAL>closure {σ, swap x (σ x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = ⊤<VAR>x : α<VAR>H : Subgroup (Perm α) := closure {σ, swap x (σ x)}<VAR>h3 : σ ∈ H<VAR>h4 : swap x (σ x) ∈ H<VAR>step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H<VAR>step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H<VAR>step3 : ∀ (y : α), swap x y ∈ H<VAR>step4 : ∀ (y z : α), swap y z ∈ H<GOAL>closure {σ, swap x (σ x)} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Finite β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>σ : Perm α<VAR>h1 : σ.IsCycle<VAR>h2 : σ.support = ⊤<VAR>x : α<VAR>H : Subgroup (Perm α) := closure {σ, swap x (σ x)}<VAR>h3 : σ ∈ H<VAR>h4 : swap x (σ x) ∈ H<VAR>step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H<VAR>step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H<VAR>step3 : ∀ (y : α), swap x y ∈ H<VAR>step4 : ∀ (y z : α), swap y z ∈ H<GOAL>{σ | σ.IsSwap} ⊆ ↑(closure {σ, swap x (σ x)})
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace α'<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace β'<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝ : NormedAddCommGroup E<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>hC : generateFrom C = inst✝⁵<VAR>hD : generateFrom D = inst✝³<VAR>h2C : IsCountablySpanning C<VAR>h2D : IsCountablySpanning D<GOAL>generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D) = Prod.instMeasurableSpace
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent (ι := ↑s) R Subtype.val<GOAL>∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndependent (ι := ↑t) R Subtype.val
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent (ι := ↑s) R Subtype.val<VAR>t : Set (M ⧸ Submodule.span R s)<VAR>ht : #↑t = Module.rank R (M ⧸ Submodule.span R s)<VAR>ht' : LinearIndependent (ι := ↑t) R Subtype.val<GOAL>∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndependent (ι := ↑t) R Subtype.val
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent (ι := ↑s) R Subtype.val<VAR>t : Set (M ⧸ Submodule.span R s)<VAR>ht : #↑t = Module.rank R (M ⧸ Submodule.span R s)<VAR>ht' : LinearIndependent (ι := ↑t) R Subtype.val<VAR>sec : M ⧸ Submodule.span R s → M<VAR>hsec : ∀ (b : M ⧸ Submodule.span R s), Submodule.Quotient.mk (sec b) = b<GOAL>∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndependent (ι := ↑t) R Subtype.val
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent (ι := ↑s) R Subtype.val<VAR>t : Set (M ⧸ Submodule.span R s)<VAR>ht : #↑t = Module.rank R (M ⧸ Submodule.span R s)<VAR>ht' : LinearIndependent (ι := ↑t) R Subtype.val<VAR>sec : M ⧸ Submodule.span R s → M<VAR>hsec : ∀ (b : M ⧸ Submodule.span R s), Submodule.Quotient.mk (sec b) = b<VAR>hsec' : Submodule.Quotient.mk ∘ sec = id<GOAL>∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndependent (ι := ↑t) R Subtype.val
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent (ι := ↑s) R Subtype.val<VAR>t : Set (M ⧸ Submodule.span R s)<VAR>ht : #↑t = Module.rank R (M ⧸ Submodule.span R s)<VAR>ht' : LinearIndependent (ι := ↑t) R Subtype.val<VAR>sec : M ⧸ Submodule.span R s → M<VAR>hsec : ∀ (b : M ⧸ Submodule.span R s), Submodule.Quotient.mk (sec b) = b<VAR>hsec' : Submodule.Quotient.mk ∘ sec = id<VAR>hst : Disjoint s (sec '' t)<GOAL>∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndependent (ι := ↑t) R Subtype.val
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent (ι := ↑s) R Subtype.val<VAR>t : Set (M ⧸ Submodule.span R s)<VAR>ht : #↑t = Module.rank R (M ⧸ Submodule.span R s)<VAR>ht' : LinearIndependent (ι := ↑t) R Subtype.val<VAR>sec : M ⧸ Submodule.span R s → M<VAR>hsec : ∀ (b : M ⧸ Submodule.span R s), Submodule.Quotient.mk (sec b) = b<VAR>hsec' : Submodule.Quotient.mk ∘ sec = id<VAR>hst : Disjoint s (sec '' t)<GOAL>#↑(s ∪ sec '' t) = Module.rank R M
<VAR>R : Type u_1<VAR>M M₁ M₂ M₃ : Type u<VAR>M' : Type v<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup M₁<VAR>inst✝⁹ : AddCommGroup M₂<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M'<VAR>inst✝¹ : HasRankNullity.{u, u_1} R<VAR>inst✝ : StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent (ι := ↑s) R Subtype.val<VAR>t : Set (M ⧸ Submodule.span R s)<VAR>ht : #↑t = Module.rank R (M ⧸ Submodule.span R s)<VAR>ht' : LinearIndependent (ι := ↑t) R Subtype.val<VAR>sec : M ⧸ Submodule.span R s → M<VAR>hsec : ∀ (b : M ⧸ Submodule.span R s), Submodule.Quotient.mk (sec b) = b<VAR>hsec' : Submodule.Quotient.mk ∘ sec = id<VAR>hst : Disjoint s (sec '' t)<GOAL>LinearIndependent (ι := ↑(s ∪ sec '' t)) R Subtype.val
<VAR>α : Type u_1<VAR>inst✝ : AddCommMonoid α<VAR>c : ℕ<GOAL>smul c 0 = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>h3 : 0 < 3<VAR>h23 : 0 < 2 / 3<GOAL>∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>h3 : 0 < 3<VAR>h23 : 0 < 2 / 3<GOAL>∃ g, ‖g‖ ≤ ‖0‖ / 3 ∧ dist (g.compContinuous e) 0 ≤ 2 / 3 * ‖0‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>h3 : 0 < 3<VAR>h23 : 0 < 2 / 3<VAR>hf : f ≠ 0<GOAL>∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>h3 : 0 < 3<VAR>h23 : 0 < 2 / 3<VAR>hf : 0 < ‖f‖<GOAL>∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>h3 : 0 < 3<VAR>h23 : 0 < 2 / 3<VAR>hf : 0 < ‖f‖<VAR>hf3 : -‖f‖ / 3 < ‖f‖ / 3<GOAL>∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>h3 : 0 < 3<VAR>h23 : 0 < 2 / 3<VAR>hf : 0 < ‖f‖<VAR>hf3 : -‖f‖ / 3 < ‖f‖ / 3<VAR>hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))<GOAL>∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>h3 : 0 < 3<VAR>h23 : 0 < 2 / 3<VAR>hf : 0 < ‖f‖<VAR>hf3 : -‖f‖ / 3 < ‖f‖ / 3<VAR>hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))<VAR>hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))<GOAL>∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>h3 : 0 < 3<VAR>h23 : 0 < 2 / 3<VAR>hf : 0 < ‖f‖<VAR>hf3 : -‖f‖ / 3 < ‖f‖ / 3<VAR>hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))<VAR>hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))<VAR>hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))<GOAL>∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X →ᵇ ℝ<VAR>e : C(X, Y)<VAR>he : ClosedEmbedding ⇑e<VAR>h3 : 0 < 3<VAR>h23 : 0 < 2 / 3<VAR>hf : 0 < ‖f‖<VAR>hf3 : -‖f‖ / 3 < ‖f‖ / 3<VAR>hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))<VAR>hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))<VAR>hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))<VAR>g : Y →ᵇ ℝ<VAR>hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))<VAR>hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))<VAR>hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)<GOAL>∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝ : AddCommMonoid α<VAR>hf : Periodic f c<VAR>x : α<VAR>m : ℕ<GOAL>f (⟨(fun i => i • c) m, ⋯⟩ +ᵥ x) = f x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List α<GOAL>indexOf a (a :: l) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a < b * a ↔ 1 * a < b * a
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>e : σ →₀ ℕ<VAR>s : S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(rTensor ((monomial e) s ⊗ₜ[R] n)) d = if e = d then s ⊗ₜ[R] n else 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>inst✝³ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝² : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 β<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>c : 𝕜<GOAL>DominatedFinMeasAdditive μ (fun s => c • T s) (‖c‖ * C)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>inst✝³ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝² : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 β<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>c : 𝕜<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>‖(fun s => c • T s) s‖ ≤ ‖c‖ * C * (μ s).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>inst✝³ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝² : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 β<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>c : 𝕜<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>‖c • T s‖ ≤ ‖c‖ * C * (μ s).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>inst✝³ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝² : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 β<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>c : 𝕜<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<GOAL>‖c‖ * ‖T s‖ ≤ ‖c‖ * (C * (μ s).toReal)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s✝ : Set α<VAR>t : Set β<VAR>s : Set α<VAR>f : Filter α<GOAL>map Subtype.val (comap Subtype.val f) = f ⊓ 𝓟 s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : Group α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a✝¹ : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>a✝ : α<GOAL>a✝ ∈ (a • s)⁻¹ ↔ a✝ ∈ op a⁻¹ • s⁻¹
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<GOAL>max (μ univ) (ν univ) < ⊤
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x x₀ : M<VAR>y₀ : M'<GOAL>mfderiv I' (I.prod I') (fun y => (x₀, y)) y₀ = ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x x₀ : M<VAR>y₀ : M'<GOAL>(mfderiv I' I (fun x => x₀) y₀).prod (mfderiv I' I' id y₀) = ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<GOAL>(coeff R 0) X = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>s : σ<VAR>φ : MvPowerSeries σ R<GOAL>X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff R m) φ = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>s : σ<VAR>φ : MvPowerSeries σ R<GOAL>(∀ (m : σ →₀ ℕ), m s < 1 → (coeff R m) φ = 0) ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff R m) φ = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>s : Finset ι<VAR>v : ι → E<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ s, 0 ≤ w i<VAR>hw₁ : s.sum w = 1<GOAL>(affineCombination R s v) w ∈ (convexHull R) (Set.range v)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>s : Finset ι<VAR>v : ι → E<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ s, 0 ≤ w i<VAR>hw₁ : s.sum w = 1<GOAL>s.centerMass w v ∈ (convexHull R) (Set.range v)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>s : Finset ι<VAR>v : ι → E<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ s, 0 ≤ w i<VAR>hw₁ : s.sum w = 1<GOAL>0 < ∑ i ∈ s, w i
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w✝ : ι → R<VAR>z : ι → E<VAR>s : Finset ι<VAR>v : ι → E<VAR>w : ι → R<VAR>hw₀ : ∀ i ∈ s, 0 ≤ w i<VAR>hw₁ : s.sum w = 1<GOAL>∀ i ∈ s, v i ∈ Set.range v
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>s : Set R[X]<VAR>s_fin : s.Finite<GOAL>∃ n, Submodule.span R s ≤ degreeLT R n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>s : Set R[X]<VAR>s_fin : s.Finite<VAR>n : ℕ<VAR>h✝ : Submodule.span R s ≤ degreeLE R ↑n<GOAL>∃ n, Submodule.span R s ≤ degreeLT R n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>f : α' → α<VAR>a✝ : α'<GOAL>(Finsupp.total α' M R (v ∘ f) ∘ₗ lsingle a✝) 1 = ((Finsupp.total α M R v ∘ₗ lmapDomain R R f) ∘ₗ lsingle a✝) 1