ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>c : R<GOAL>(⇑derivative)^[n] ((X - C c) ^ n) = ↑n.factorial
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<VAR>p : P<GOAL>affineSpan ℝ {p, s.points i} = s.altitude i ↔ p ≠ s.points i ∧ p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' ↑(univ.erase i))).directionᗮ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P (n + 1)<VAR>i : Fin (n + 2)<VAR>p : P<GOAL>vectorSpan ℝ {p, s.points i} = (s.altitude i).direction ↔ p ≠ s.points i ∧ p -ᵥ s.points i ∈ vectorSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (vectorSpan ℝ (s.points '' ↑(univ.erase i)))ᗮ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S✝ : Submonoid M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>S : Set (RingCon R)<GOAL>sSup S = ringConGen (sSup (DFunLike.coe '' S))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>S : Set (RingCon R)<GOAL>(ringConGen fun x y => ∃ c ∈ S, c x y) = ringConGen (⨆ a ∈ S, ⇑a)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Add R<VAR>inst✝ : Mul R<VAR>S : Set (RingCon R)<VAR>x y : R<GOAL>(∃ c ∈ S, c x y) ↔ (⨆ a ∈ S, ⇑a) x y
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<GOAL>map N.incl (lowerCentralSeries R L (↥↑N) k) = lcs k N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>k : ℕ<VAR>N : LieSubmodule R L M<GOAL>lcs k N ≤ N
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp (a - p) b = toIocMod hp a b - p
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>δ : ℝ<VAR>hδ : 0 ≤ δ<VAR>y : α<GOAL>y ∈ cthickening δ {x} ↔ y ∈ closedBall x δ
<VAR>α : Type u_1<VAR>s✝¹ t✝¹ : Finset α<VAR>n✝ : ?m.33453<VAR>s✝ t✝ : Finset α<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>n : ℕ<VAR>s : Finset α<VAR>t : Finset β<GOAL>t ∈ powersetCard n (map f s) ↔ t ∈ map (mapEmbedding f).toEmbedding (powersetCard n s)
<VAR>α : Type u_1<VAR>s✝¹ t✝¹ : Finset α<VAR>n✝ : ?m.33453<VAR>s✝ t✝ : Finset α<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>n : ℕ<VAR>s : Finset α<VAR>t : Finset β<GOAL>t ⊆ map f s ∧ t.card = n ↔ ∃ a, (a ⊆ s ∧ a.card = n) ∧ (mapEmbedding f).toEmbedding a = t
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>n : ℕ<GOAL>toZ i0 (succ^[n] i0) ≤ ↑n
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>n : ℕ<GOAL>↑(Nat.find ⋯) ≤ ↑n
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>n : ℕ<GOAL>Nat.find ⋯ ≤ n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₃ : A ⟶ S.L₀.X₃<VAR>x₂ : A ⟶ S.L₁.X₂<VAR>x₁ : A ⟶ S.L₂.X₁<VAR>h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃<VAR>h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂<GOAL>x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₃ : A ⟶ S.L₀.X₃<VAR>x₂ : A ⟶ S.L₁.X₂<VAR>x₁ : A ⟶ S.L₂.X₁<VAR>h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃<VAR>h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂<VAR>H : pullback.lift x₂ x₃ h₂ ≫ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁<GOAL>x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₃ : A ⟶ S.L₀.X₃<VAR>x₂ : A ⟶ S.L₁.X₂<VAR>x₁ : A ⟶ S.L₂.X₁<VAR>h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃<VAR>h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂<VAR>H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁<GOAL>x₃ ≫ S.δ = x₁ ≫ S.v₂₃.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₃ : A ⟶ S.L₀.X₃<VAR>x₂ : A ⟶ S.L₁.X₂<VAR>x₁ : A ⟶ S.L₂.X₁<VAR>h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃<VAR>h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂<VAR>H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁<GOAL>(pullback.lift x₂ x₃ h₂ ≫ S.φ₁) ≫ S.v₂₃.τ₁ = x₁ ≫ S.v₂₃.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<VAR>A : C<VAR>x₃ : A ⟶ S.L₀.X₃<VAR>x₂ : A ⟶ S.L₁.X₂<VAR>x₁ : A ⟶ S.L₂.X₁<VAR>h₂ : x₂ ≫ S.L₁.g = x₃ ≫ S.v₀₁.τ₃<VAR>h₁ : x₁ ≫ S.L₂.f = x₂ ≫ S.v₁₂.τ₂<VAR>H : x₃ ≫ S.δ = pullback.lift x₂ x₃ h₂ ≫ S.φ₁ ≫ S.v₂₃.τ₁<GOAL>pullback.lift x₂ x₃ h₂ ≫ S.φ₁ = x₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hY : AEMeasurable Y μ<VAR>hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂(condDistrib Y X μ) x) (Measure.map X μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hY : AEMeasurable Y μ<VAR>hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>AEStronglyMeasurable (fun x => ∫ (y : Ω), f (x, y) ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x) (Measure.map (fun a => (X a, Y a)) μ).fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<GOAL>(2 * dValue N - 1) ^ nValue N ≤ N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<VAR>this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N<GOAL>(2 * dValue N - 1) ^ nValue N ≤ N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<VAR>this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N<GOAL>(2 * ↑(dValue N)) ^ nValue N ≤ ↑N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<VAR>this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N<GOAL>2 * ↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<VAR>this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N<GOAL>↑(dValue N) ≤ ↑N ^ (↑(nValue N))⁻¹ / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN : 2 ≤ N<VAR>this : (2 * dValue N - 1) ^ nValue N ≤ (2 * dValue N) ^ nValue N<GOAL>0 < 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>c : Cardinal.{u_3}<VAR>n : ℕ<GOAL>toPartENat c = ↑n ↔ c = ↑n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<GOAL>∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ ((P.equivSigmaParts.trans ((Equiv.refl { x // x ∈ P.parts }).sigmaCongr fun t => (↑t).equivFin)) a).fst = ((P.equivSigmaParts.trans ((Equiv.refl { x // x ∈ P.parts }).sigmaCongr fun t => (↑t).equivFin)) b).fst
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<GOAL>univ.pi t = ∅ ↔ ∃ i, t i = ∅
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<VAR>x₀ : G<GOAL>𝓝 x₀ = B.N x₀
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<VAR>x₀ : G<GOAL>∀ (a : G), ∀ i ∈ toFilterBasis, a ∈ (fun y => a * y) '' id i
<VAR>G : Type u<VAR>inst✝ : Group G<VAR>B✝ B : GroupFilterBasis G<VAR>x₀ : G<GOAL>∀ (a : G), ∀ i ∈ toFilterBasis, ∀ᶠ (x : G) in map (fun y => a * y) toFilterBasis.filter, (fun y => a * y) '' id i ∈ map (fun y => x * y) toFilterBasis.filter
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : MulAction R M<VAR>inst✝² : Monoid M<VAR>inst✝¹ : IsScalarTower R M M<VAR>inst✝ : SMulCommClass R M M<VAR>p : SubMulAction R M<GOAL>↑p ^ 0 ⊆ ↑(p ^ 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : MulAction R M<VAR>inst✝² : Monoid M<VAR>inst✝¹ : IsScalarTower R M M<VAR>inst✝ : SMulCommClass R M M<VAR>p : SubMulAction R M<GOAL>1 ⊆ ↑1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Monoid R<VAR>inst✝³ : MulAction R M<VAR>inst✝² : Monoid M<VAR>inst✝¹ : IsScalarTower R M M<VAR>inst✝ : SMulCommClass R M M<VAR>p : SubMulAction R M<VAR>n : ℕ<GOAL>↑p ^ (n + 1) ⊆ ↑(p ^ (n + 1))
<VAR>x y : ℂ<GOAL>tanh (x * I) = tan x * I
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : Set (Subsemigroup M)<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<GOAL>cfc (fun x => star x) a = star a
<VAR>x✝ y✝ x y : ℝ<VAR>h : √x < y<GOAL>x < y ^ 2
<VAR>x✝ y✝ x y : ℝ<VAR>h : √x < y<VAR>hy : 0 < y<GOAL>x < y ^ 2
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a✝ a : ℕ<GOAL>↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡ ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑(∏ i ∈ range a.succ, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a✝ a : ℕ<GOAL>↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡ ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a✝ a : ℕ<GOAL>↑((n / p ^ a).choose (k / p ^ a)) ≡ ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a✝ a : ℕ<GOAL>↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / p ^ a / p).choose (k / p ^ a / p)) ≡ ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) * ↑((n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a✝ a : ℕ<GOAL>↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / (p * p ^ a)).choose (k / (p * p ^ a))) ≡ ↑((n / p ^ a % p).choose (k / p ^ a % p)) * ↑((n / (p * p ^ a)).choose (k / (p * p ^ a))) [ZMOD ↑p]
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>h : I = 0<VAR>x : K<GOAL>↑(re x) = x
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>h : I = 0<VAR>x : K<GOAL>↑(re x) = ↑(re x) + ↑(im x) * I
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>h : I = 0<GOAL>∀ (x y : K), { toFun := ⇑re, invFun := ofReal, left_inv := ⋯, right_inv := ⋯ }.toFun (x * y) = { toFun := ⇑re, invFun := ofReal, left_inv := ⋯, right_inv := ⋯ }.toFun x * { toFun := ⇑re, invFun := ofReal, left_inv := ⋯, right_inv := ⋯ }.toFun y
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>p q : List (Symbol T N)<GOAL>r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f : GromovHausdorff.Cb X Y<VAR>C : ℝ<GOAL>BddAbove (range fun y => ⨅ x, f (inl x, inr y) + C)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>f : GromovHausdorff.Cb X Y<VAR>C Cf : ℝ<VAR>hCf : Cf ∈ upperBounds (range ⇑f)<GOAL>BddAbove (range fun y => ⨅ x, f (inl x, inr y) + C)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f✝ : GromovHausdorff.ProdSpaceFun X Y<VAR>x y✝ z t : X ⊕ Y<VAR>f : GromovHausdorff.Cb X Y<VAR>C Cf : ℝ<VAR>hCf : Cf ∈ upperBounds (range ⇑f)<VAR>y : Y<GOAL>⨅ x, f (inl x, inr y) + C ≤ Cf + C
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<GOAL>Convex 𝕜 s ↔ s.OrdConnected
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f✝ g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>f : X → Y → Z<VAR>hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d<GOAL>Continuous (uncurry (lift₂ f hf)) ↔ Continuous (uncurry f)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocRing α<VAR>inst✝ : Fintype n<VAR>A : Matrix m n α<VAR>x y : n → α<VAR>x✝ : m<GOAL>(A *ᵥ (x - y)) x✝ = (A *ᵥ x - A *ᵥ y) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>H : s ≤ᶠ[ae μ] t<GOAL>μ (s ∪ t) = μ (t ∪ s \ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>H : s ≤ᶠ[ae μ] t<GOAL>μ t + μ (s \ t) = μ t
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>c : Cone F<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>c.π.app j ≫ F.map f = c.π.app j'
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>inst✝ : Category.{v₄, u₄} D<VAR>F : J ⥤ C<VAR>c : Cone F<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>((const J).obj c.pt).map f ≫ c.π.app j' = c.π.app j'
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>Y : C<VAR>P : Subobject Y<GOAL>IsIso P.arrow ↔ P = ⊤
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹¹ : EMetricSpace X<VAR>inst✝¹⁰ : EMetricSpace Y<VAR>inst✝⁹ : MeasurableSpace X<VAR>inst✝⁸ : BorelSpace X<VAR>inst✝⁷ : MeasurableSpace Y<VAR>inst✝⁶ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace P<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor E P<VAR>inst✝ : BorelSpace P<VAR>x y : P<GOAL>μH[1] (affineSegment ℝ x y) = edist x y
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹¹ : EMetricSpace X<VAR>inst✝¹⁰ : EMetricSpace Y<VAR>inst✝⁹ : MeasurableSpace X<VAR>inst✝⁸ : BorelSpace X<VAR>inst✝⁷ : MeasurableSpace Y<VAR>inst✝⁶ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>P : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : MeasurableSpace P<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor E P<VAR>inst✝ : BorelSpace P<VAR>x y : P<GOAL>(algebraMap ℝ≥0 ℝ≥0∞) (nndist x y) = edist x y
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<GOAL>idealOfSet 𝕜 (setOfIdeal I) = I.closure
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<GOAL>idealOfSet 𝕜 (setOfIdeal I) ≤ I.closure
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ b ∈ ↑I, dist f b < ε
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : ↑ε > 0<GOAL>∃ b ∈ ↑I, dist f b < ↑ε
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<GOAL>∃ b ∈ ↑I, dist f b < ↑ε
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<GOAL>∃ b ∈ ↑I, ↑(nndist f b) < ↑ε
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>t : Set X := {x | ε / 2 ≤ ‖f x‖₊}<GOAL>∃ b ∈ ↑I, nndist f b < ε
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>t : Set X := {x | ε / 2 ≤ ‖f x‖₊}<VAR>ht : IsClosed t<GOAL>∃ b ∈ ↑I, nndist f b < ε
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>t : Set X := {x | ε / 2 ≤ ‖f x‖₊}<VAR>ht : IsClosed t<VAR>htI : Disjoint t (setOfIdeal I)ᶜ<GOAL>∃ b ∈ ↑I, nndist f b < ε
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>t : Set X := {x | ε / 2 ≤ ‖f x‖₊}<VAR>ht : IsClosed t<VAR>htI : Disjoint t (setOfIdeal I)ᶜ<VAR>g' : C(X, ℝ≥0)<VAR>hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I<VAR>hgt' : ∀ x ∈ t, 0 < g' x<GOAL>∃ g, (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I ∧ (∀ (x : X), g x ≤ 1) ∧ Set.EqOn (⇑g) 1 t
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>t : Set X := {x | ε / 2 ≤ ‖f x‖₊}<VAR>ht : IsClosed t<VAR>htI : Disjoint t (setOfIdeal I)ᶜ<VAR>g' : C(X, ℝ≥0)<VAR>hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I<VAR>hgt' : ∀ x ∈ t, 0 < g' x<VAR>c : ℝ≥0<VAR>hc : c > 0<VAR>hgc' : ∀ y ∈ t, c ≤ g' y<GOAL>∃ g, (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I ∧ (∀ (x : X), g x ≤ 1) ∧ Set.EqOn (⇑g) 1 t
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>t : Set X := {x | ε / 2 ≤ ‖f x‖₊}<VAR>ht : IsClosed t<VAR>htI : Disjoint t (setOfIdeal I)ᶜ<VAR>g' : C(X, ℝ≥0)<VAR>hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I<VAR>hgt' : ∀ x ∈ t, 0 < g' x<VAR>c : ℝ≥0<VAR>hc : c > 0<VAR>hgc' : ∀ y ∈ t, c ≤ g' y<VAR>g : C(X, ℝ≥0)<VAR>hg : ∀ (x : X), (g * g') x ≤ 1<VAR>hgc : Set.EqOn (⇑(g * g')) 1 {x | c ≤ g' x}<GOAL>∃ g, (↑(algebraMapCLM ℝ≥0 𝕜)).comp g ∈ I ∧ (∀ (x : X), g x ≤ 1) ∧ Set.EqOn (⇑g) 1 t
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>t : Set X := {x | ε / 2 ≤ ‖f x‖₊}<VAR>ht : IsClosed t<VAR>htI : Disjoint t (setOfIdeal I)ᶜ<VAR>g' : C(X, ℝ≥0)<VAR>hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I<VAR>hgt' : ∀ x ∈ t, 0 < g' x<VAR>c : ℝ≥0<VAR>hc : c > 0<VAR>hgc' : ∀ y ∈ t, c ≤ g' y<VAR>g : C(X, ℝ≥0)<VAR>hg : ∀ (x : X), (g * g') x ≤ 1<VAR>hgc : Set.EqOn (⇑(g * g')) 1 {x | c ≤ g' x}<GOAL>(↑(algebraMapCLM ℝ≥0 𝕜)).comp (g * g') ∈ I
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>t : Set X := {x | ε / 2 ≤ ‖f x‖₊}<VAR>ht : IsClosed t<VAR>htI : Disjoint t (setOfIdeal I)ᶜ<VAR>g' : C(X, ℝ≥0)<VAR>hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I<VAR>hgt' : ∀ x ∈ t, 0 < g' x<VAR>c : ℝ≥0<VAR>hc : c > 0<VAR>hgc' : ∀ y ∈ t, c ≤ g' y<VAR>g : C(X, ℝ≥0)<VAR>hg : ∀ (x : X), (g * g') x ≤ 1<VAR>hgc : Set.EqOn (⇑(g * g')) 1 {x | c ≤ g' x}<GOAL>(↑(algebraMapCLM ℝ≥0 𝕜)).comp (g * g') = (↑(algebraMapCLM ℝ≥0 𝕜)).comp g * (↑(algebraMapCLM ℝ≥0 𝕜)).comp g'
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : CompactSpace X<VAR>inst✝ : T2Space X<VAR>I : Ideal C(X, 𝕜)<VAR>f : C(X, 𝕜)<VAR>hf : f ∈ idealOfSet 𝕜 (setOfIdeal I)<VAR>ε : ℝ≥0<VAR>hε : 0 < ε<VAR>t : Set X := {x | ε / 2 ≤ ‖f x‖₊}<VAR>ht : IsClosed t<VAR>htI : Disjoint t (setOfIdeal I)ᶜ<VAR>g' : C(X, ℝ≥0)<VAR>hI' : (↑(algebraMapCLM ℝ≥0 𝕜)).comp g' ∈ I<VAR>hgt' : ∀ x ∈ t, 0 < g' x<VAR>c : ℝ≥0<VAR>hc : c > 0<VAR>hgc' : ∀ y ∈ t, c ≤ g' y<VAR>g : C(X, ℝ≥0)<VAR>hg : ∀ (x : X), (g * g') x ≤ 1<VAR>hgc : Set.EqOn (⇑(g * g')) 1 {x | c ≤ g' x}<VAR>a✝ : X<GOAL>((↑(algebraMapCLM ℝ≥0 𝕜)).comp (g * g')) a✝ = ((↑(algebraMapCLM ℝ≥0 𝕜)).comp g * (↑(algebraMapCLM ℝ≥0 𝕜)).comp g') a✝
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<VAR>f' : TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, E') (f x)<GOAL>HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f' ↔ HasFDerivAt f f' x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>this : TopologicalSpace Y := ⊥<GOAL>(range f).Finite
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>f : X → Y<VAR>hf : IsLocallyConstant f<VAR>this✝ : TopologicalSpace Y := ⊥<VAR>this : DiscreteTopology Y<GOAL>(range f).Finite