ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u<VAR>SubNegMonoid M<VAR>PseudoEMetricSpace M<VAR>IsometricVAdd Mᵃᵒᵖ M<VAR>a b c : M<GOAL>edist (a - c) (b - c) = edist a b
<VAR>M : Type u<VAR>DivInvMonoid M<VAR>PseudoEMetricSpace M<VAR>IsometricSMul Mᵐᵒᵖ M<VAR>a b c : M<GOAL>edist (a / c) (b / c) = edist a b
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<GOAL>edist a⁻¹ b⁻¹ = edist a b
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b : G<GOAL>edist (-a) (-b) = edist a b
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<GOAL>Isometry Neg.neg
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<GOAL>Isometry Inv.inv
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>x y : G<GOAL>edist x⁻¹ y = edist x y⁻¹
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>x y : G<GOAL>edist (-x) y = edist x (-y)
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b c : G<GOAL>edist (a - b) (a - c) = edist b c
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b c : G<GOAL>edist (a / b) (a / c) = edist b c
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<GOAL>(IsometryEquiv.constVAdd c) x = c +ᵥ x
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<GOAL>(IsometryEquiv.constSMul c).toEquiv = MulAction.toPerm c
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<GOAL>(IsometryEquiv.constVAdd c).toEquiv = AddAction.toPerm c
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<GOAL>(IsometryEquiv.constSMul c) x = c • x
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<GOAL>(IsometryEquiv.constVAdd c).symm = IsometryEquiv.constVAdd (-c)
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<GOAL>(IsometryEquiv.constSMul c).symm = IsometryEquiv.constSMul c⁻¹
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>c : G<GOAL>(IsometryEquiv.addLeft c).toEquiv = Equiv.addLeft c
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>c x : G<GOAL>(IsometryEquiv.mulLeft c) x = c * x
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>c x : G<GOAL>(IsometryEquiv.addLeft c) x = c + x
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>c : G<GOAL>(IsometryEquiv.mulLeft c).toEquiv = Equiv.mulLeft c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>x : G<GOAL>(IsometryEquiv.addLeft x).symm = IsometryEquiv.addLeft (-x)
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>x : G<GOAL>(IsometryEquiv.mulLeft x).symm = IsometryEquiv.mulLeft x⁻¹
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>c : G<GOAL>(IsometryEquiv.addRight c).toEquiv = Equiv.addRight c
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>c x : G<GOAL>(IsometryEquiv.mulRight c) x = x * c
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>c : G<GOAL>(IsometryEquiv.mulRight c).toEquiv = Equiv.mulRight c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>c x : G<GOAL>(IsometryEquiv.addRight c) x = x + c
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>x : G<GOAL>(IsometryEquiv.mulRight x).symm = IsometryEquiv.mulRight x⁻¹
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>x : G<GOAL>(IsometryEquiv.addRight x).symm = IsometryEquiv.addRight (-x)
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>c b : G<GOAL>(IsometryEquiv.divRight c) b = b / c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>c : G<GOAL>(IsometryEquiv.subRight c).toEquiv = Equiv.subRight c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>c b : G<GOAL>(IsometryEquiv.subRight c) b = b - c
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>c : G<GOAL>(IsometryEquiv.divRight c).toEquiv = Equiv.divRight c
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>c : G<GOAL>(IsometryEquiv.divRight c).symm = IsometryEquiv.mulRight c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>c : G<GOAL>(IsometryEquiv.subRight c).symm = IsometryEquiv.addRight c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>c : G<GOAL>(IsometryEquiv.subLeft c).toEquiv = Equiv.subLeft c
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>c : G<GOAL>(IsometryEquiv.divLeft c).toEquiv = Equiv.divLeft c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>c b : G<GOAL>(IsometryEquiv.subLeft c).symm b = -b + c
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>c b : G<GOAL>(IsometryEquiv.divLeft c) b = c / b
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>c b : G<GOAL>(IsometryEquiv.subLeft c) b = c - b
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>c b : G<GOAL>(IsometryEquiv.divLeft c).symm b = b⁻¹ * c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<GOAL>(IsometryEquiv.neg G).toEquiv = Equiv.neg G
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<GOAL>(IsometryEquiv.inv G).toEquiv = Equiv.inv G
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<GOAL>∀ (a : G), (IsometryEquiv.neg G) a = -a
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<GOAL>∀ (a : G), (IsometryEquiv.inv G) a = a⁻¹
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<GOAL>(IsometryEquiv.inv G).symm = IsometryEquiv.inv G
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<GOAL>(IsometryEquiv.neg G).symm = IsometryEquiv.neg G
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>c +ᵥ EMetric.ball x r = EMetric.ball (c +ᵥ x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>c • EMetric.ball x r = EMetric.ball (c • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>(fun x => c +ᵥ x) ⁻¹' EMetric.ball x r = EMetric.ball (-c +ᵥ x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>(fun x => c • x) ⁻¹' EMetric.ball x r = EMetric.ball (c⁻¹ • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>c • EMetric.closedBall x r = EMetric.closedBall (c • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>c +ᵥ EMetric.closedBall x r = EMetric.closedBall (c +ᵥ x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>(fun x => c • x) ⁻¹' EMetric.closedBall x r = EMetric.closedBall (c⁻¹ • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoEMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ≥0∞<GOAL>(fun x => c +ᵥ x) ⁻¹' EMetric.closedBall x r = EMetric.closedBall (-c +ᵥ x) r
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => a + x) ⁻¹' EMetric.ball b r = EMetric.ball (-a + b) r
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => a * x) ⁻¹' EMetric.ball b r = EMetric.ball (a⁻¹ * b) r
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => x * a) ⁻¹' EMetric.ball b r = EMetric.ball (b / a) r
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => x + a) ⁻¹' EMetric.ball b r = EMetric.ball (b - a) r
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul G G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => a * x) ⁻¹' EMetric.closedBall b r = EMetric.closedBall (a⁻¹ * b) r
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd G G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => a + x) ⁻¹' EMetric.closedBall b r = EMetric.closedBall (-a + b) r
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoEMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => x + a) ⁻¹' EMetric.closedBall b r = EMetric.closedBall (b - a) r
<VAR>G : Type v<VAR>Group G<VAR>PseudoEMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ≥0∞<GOAL>(fun x => x * a) ⁻¹' EMetric.closedBall b r = EMetric.closedBall (b / a) r
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>SMul M X<VAR>IsometricSMul M X<VAR>c : M<VAR>x y : X<GOAL>dist (c • x) (c • y) = dist x y
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>VAdd M X<VAR>IsometricVAdd M X<VAR>c : M<VAR>x y : X<GOAL>dist (c +ᵥ x) (c +ᵥ y) = dist x y
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>SMul M X<VAR>IsometricSMul M X<VAR>c : M<VAR>x y : X<GOAL>nndist (c • x) (c • y) = nndist x y
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>VAdd M X<VAR>IsometricVAdd M X<VAR>c : M<VAR>x y : X<GOAL>nndist (c +ᵥ x) (c +ᵥ y) = nndist x y
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>VAdd M X<VAR>IsometricVAdd M X<VAR>c : M<VAR>s : Set X<GOAL>Metric.diam (c +ᵥ s) = Metric.diam s
<VAR>M : Type u<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>SMul M X<VAR>IsometricSMul M X<VAR>c : M<VAR>s : Set X<GOAL>Metric.diam (c • s) = Metric.diam s
<VAR>M : Type u<VAR>PseudoMetricSpace M<VAR>Add M<VAR>IsometricVAdd M M<VAR>a b c : M<GOAL>dist (a + b) (a + c) = dist b c
<VAR>M : Type u<VAR>PseudoMetricSpace M<VAR>Mul M<VAR>IsometricSMul M M<VAR>a b c : M<GOAL>dist (a * b) (a * c) = dist b c
<VAR>M : Type u<VAR>PseudoMetricSpace M<VAR>Add M<VAR>IsometricVAdd M M<VAR>a b c : M<GOAL>nndist (a + b) (a + c) = nndist b c
<VAR>M : Type u<VAR>PseudoMetricSpace M<VAR>Mul M<VAR>IsometricSMul M M<VAR>a b c : M<GOAL>nndist (a * b) (a * c) = nndist b c
<VAR>M : Type u<VAR>Add M<VAR>PseudoMetricSpace M<VAR>IsometricVAdd Mᵃᵒᵖ M<VAR>a b c : M<GOAL>dist (a + c) (b + c) = dist a b
<VAR>M : Type u<VAR>Mul M<VAR>PseudoMetricSpace M<VAR>IsometricSMul Mᵐᵒᵖ M<VAR>a b c : M<GOAL>dist (a * c) (b * c) = dist a b
<VAR>M : Type u<VAR>PseudoMetricSpace M<VAR>Add M<VAR>IsometricVAdd Mᵃᵒᵖ M<VAR>a b c : M<GOAL>nndist (a + c) (b + c) = nndist a b
<VAR>M : Type u<VAR>PseudoMetricSpace M<VAR>Mul M<VAR>IsometricSMul Mᵐᵒᵖ M<VAR>a b c : M<GOAL>nndist (a * c) (b * c) = nndist a b
<VAR>M : Type u<VAR>SubNegMonoid M<VAR>PseudoMetricSpace M<VAR>IsometricVAdd Mᵃᵒᵖ M<VAR>a b c : M<GOAL>dist (a - c) (b - c) = dist a b
<VAR>M : Type u<VAR>DivInvMonoid M<VAR>PseudoMetricSpace M<VAR>IsometricSMul Mᵐᵒᵖ M<VAR>a b c : M<GOAL>dist (a / c) (b / c) = dist a b
<VAR>M : Type u<VAR>SubNegMonoid M<VAR>PseudoMetricSpace M<VAR>IsometricVAdd Mᵃᵒᵖ M<VAR>a b c : M<GOAL>nndist (a - c) (b - c) = nndist a b
<VAR>M : Type u<VAR>DivInvMonoid M<VAR>PseudoMetricSpace M<VAR>IsometricSMul Mᵐᵒᵖ M<VAR>a b c : M<GOAL>nndist (a / c) (b / c) = nndist a b
<VAR>G : Type v<VAR>Group G<VAR>PseudoMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<GOAL>dist a⁻¹ b⁻¹ = dist a b
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b : G<GOAL>dist (-a) (-b) = dist a b
<VAR>G : Type v<VAR>Group G<VAR>PseudoMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<GOAL>nndist a⁻¹ b⁻¹ = nndist a b
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b : G<GOAL>nndist (-a) (-b) = nndist a b
<VAR>G : Type v<VAR>Group G<VAR>PseudoMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b c : G<GOAL>dist (a / b) (a / c) = dist b c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b c : G<GOAL>dist (a - b) (a - c) = dist b c
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoMetricSpace G<VAR>IsometricVAdd G G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b c : G<GOAL>nndist (a - b) (a - c) = nndist b c
<VAR>G : Type v<VAR>Group G<VAR>PseudoMetricSpace G<VAR>IsometricSMul G G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b c : G<GOAL>nndist (a / b) (a / c) = nndist b c
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>VAdd G X<VAR>IsometricVAdd G X<VAR>s : Set X<VAR>hs : Bornology.IsBounded s<VAR>c : G<GOAL>Bornology.IsBounded (c +ᵥ s)
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>SMul G X<VAR>IsometricSMul G X<VAR>s : Set X<VAR>hs : Bornology.IsBounded s<VAR>c : G<GOAL>Bornology.IsBounded (c • s)
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>c • Metric.ball x r = Metric.ball (c • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>c +ᵥ Metric.ball x r = Metric.ball (c +ᵥ x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>(fun x => c • x) ⁻¹' Metric.ball x r = Metric.ball (c⁻¹ • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>(fun x => c +ᵥ x) ⁻¹' Metric.ball x r = Metric.ball (-c +ᵥ x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>c +ᵥ Metric.closedBall x r = Metric.closedBall (c +ᵥ x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>c • Metric.closedBall x r = Metric.closedBall (c • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>(fun x => c • x) ⁻¹' Metric.closedBall x r = Metric.closedBall (c⁻¹ • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>(fun x => c +ᵥ x) ⁻¹' Metric.closedBall x r = Metric.closedBall (-c +ᵥ x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>c • Metric.sphere x r = Metric.sphere (c • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>c +ᵥ Metric.sphere x r = Metric.sphere (c +ᵥ x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>Group G<VAR>MulAction G X<VAR>IsometricSMul G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>(fun x => c • x) ⁻¹' Metric.sphere x r = Metric.sphere (c⁻¹ • x) r
<VAR>G : Type v<VAR>X : Type w<VAR>PseudoMetricSpace X<VAR>AddGroup G<VAR>AddAction G X<VAR>IsometricVAdd G X<VAR>c : G<VAR>x : X<VAR>r : ℝ<GOAL>(fun x => c +ᵥ x) ⁻¹' Metric.sphere x r = Metric.sphere (-c +ᵥ x) r
<VAR>G : Type v<VAR>Group G<VAR>PseudoMetricSpace G<VAR>IsometricSMul G G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => a * x) ⁻¹' Metric.ball b r = Metric.ball (a⁻¹ * b) r
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoMetricSpace G<VAR>IsometricVAdd G G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => a + x) ⁻¹' Metric.ball b r = Metric.ball (-a + b) r
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => x + a) ⁻¹' Metric.ball b r = Metric.ball (b - a) r
<VAR>G : Type v<VAR>Group G<VAR>PseudoMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => x * a) ⁻¹' Metric.ball b r = Metric.ball (b / a) r
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoMetricSpace G<VAR>IsometricVAdd G G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => a + x) ⁻¹' Metric.closedBall b r = Metric.closedBall (-a + b) r
<VAR>G : Type v<VAR>Group G<VAR>PseudoMetricSpace G<VAR>IsometricSMul G G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => a * x) ⁻¹' Metric.closedBall b r = Metric.closedBall (a⁻¹ * b) r
<VAR>G : Type v<VAR>AddGroup G<VAR>PseudoMetricSpace G<VAR>IsometricVAdd Gᵃᵒᵖ G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => x + a) ⁻¹' Metric.closedBall b r = Metric.closedBall (b - a) r
<VAR>G : Type v<VAR>Group G<VAR>PseudoMetricSpace G<VAR>IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => x * a) ⁻¹' Metric.closedBall b r = Metric.closedBall (b / a) r
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>d : ENNReal<GOAL>d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<GOAL>s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<GOAL>0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<GOAL>s.einfsep = ⊤ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ⊤
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<GOAL>s.einfsep < ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ⊤
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<GOAL>s.einfsep ≠ ⊤ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ⊤
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>d : ENNReal<GOAL>s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>hs : s.einfsep < ⊤<GOAL>s.Nontrivial
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>hs : s.einfsep ≠ ⊤<GOAL>s.Nontrivial
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>s.einfsep = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>EDist α<VAR>d : ENNReal<VAR>f : β → α<VAR>s : Set β<GOAL>d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>d : ENNReal<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hd : d ≤ s.einfsep<GOAL>d ≤ edist x y
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<GOAL>s.einfsep ≤ edist x y
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>d : ENNReal<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hxy' : edist x y ≤ d<GOAL>s.einfsep ≤ d
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>d : ENNReal<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y<GOAL>d ≤ s.einfsep
<VAR>α : Type u_1<VAR>EDist α<GOAL>∅.einfsep = ⊤
<VAR>α : Type u_1<VAR>EDist α<VAR>x : α<GOAL>{x}.einfsep = ⊤
<VAR>α : Type u_1<VAR>EDist α<VAR>ι : Type u_3<VAR>o : Option ι<VAR>s : ι → Set α<GOAL>(⋃ i ∈ o, s i).einfsep = ⨅ i ∈ o, (s i).einfsep
<VAR>α : Type u_1<VAR>EDist α<VAR>s t : Set α<VAR>hst : s ⊆ t<GOAL>t.einfsep ≤ s.einfsep
<VAR>α : Type u_1<VAR>EDist α<VAR>x : α<VAR>s : Set α<GOAL>(insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y
<VAR>α : Type u_1<VAR>EDist α<VAR>x y : α<GOAL>edist x y ⊓ edist y x ≤ {x, y}.einfsep
<VAR>α : Type u_1<VAR>EDist α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>{x, y}.einfsep ≤ edist x y
<VAR>α : Type u_1<VAR>EDist α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>{x, y}.einfsep ≤ edist y x
<VAR>α : Type u_1<VAR>EDist α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>{x, y}.einfsep = edist x y ⊓ edist y x
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<GOAL>s.einfsep = ⨅ d, Function.uncurry edist ↑d
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>DecidableEq α<VAR>Fintype ↑s<GOAL>s.einfsep = s.offDiag.toFinset.inf (Function.uncurry edist)
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>s.einfsep = ⋯.toFinset.inf (Function.uncurry edist)
<VAR>α : Type u_1<VAR>EDist α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(↑s).einfsep = s.offDiag.inf (Function.uncurry edist)
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>Finite ↑s<VAR>hs : s.Nontrivial<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>hsf : s.Finite<VAR>hs : s.Nontrivial<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>{x, y}.einfsep = edist x y
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>x : α<VAR>s : Set α<GOAL>(insert x s).einfsep = (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊓ s.einfsep
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>x y z : α<VAR>hxy : x ≠ y<VAR>hyz : y ≠ z<VAR>hxz : x ≠ z<GOAL>{x, y, z}.einfsep = edist x y ⊓ edist x z ⊓ edist y z
<VAR>β : Type u_2<VAR>π : β → Type u_3<VAR>Fintype β<VAR>(b : β) → PseudoEMetricSpace (π b)<VAR>s : (b : β) → Set (π b)<VAR>c : ENNReal<VAR>h : ∀ (b : β), c ≤ (s b).einfsep<GOAL>c ≤ (Set.univ.pi s).einfsep
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.einfsep = ⊤<GOAL>s.Subsingleton
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>s.einfsep = ⊤ ↔ s.Subsingleton
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>s.einfsep ≠ ⊤
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>s.einfsep < ⊤
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>s.einfsep < ⊤ ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<GOAL>s.einfsep ≠ ⊤ ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>d : ℝ<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y<GOAL>ENNReal.ofReal d ≤ s.einfsep
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>s : Set α<VAR>Finite ↑s<GOAL>0 < s.einfsep
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>s : Set α<VAR>Finite ↑s<GOAL>∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>0 < s.einfsep
<VAR>α : Type u_1<VAR>EMetricSpace α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<GOAL>s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ⊤
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<GOAL>0 ≤ s.infsep
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<GOAL>0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ⊤
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>s.infsep = 0
<VAR>α : Type u_1<VAR>EDist α<VAR>s : Set α<VAR>hs : 0 < s.infsep<GOAL>s.Nontrivial
<VAR>α : Type u_1<VAR>EDist α<GOAL>∅.infsep = 0
<VAR>α : Type u_1<VAR>EDist α<VAR>x : α<GOAL>{x}.infsep = 0
<VAR>α : Type u_1<VAR>EDist α<VAR>x y : α<VAR>hxy : x ≠ y<GOAL>{x, y}.infsep ≤ (edist x y ⊓ edist y x).toReal
<VAR>α : Type u_1<VAR>PseudoEMetricSpace α<VAR>x y : α<GOAL>{x, y}.infsep = (edist x y).toReal
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>d : ℝ<VAR>hs : s.Nontrivial<GOAL>d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>d : ℝ<VAR>hs : s.Nontrivial<GOAL>s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>d : ℝ<VAR>hs : s.Nontrivial<VAR>h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y<GOAL>d ≤ s.infsep
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>d : ℝ<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>hd : d ≤ s.infsep<GOAL>d ≤ dist x y