mathlib3 documentation

topology.metric_space.isometric_smul

Group actions by isometries #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define two typeclasses:

We also prove basic facts about isometric actions and define bundled isometries isometry_equiv.const_mul, isometry_equiv.mul_left, isometry_equiv.mul_right, isometry_equiv.div_left, isometry_equiv.div_right, and isometry_equiv.inv, as well as their additive versions.

If G is a group, then has_isometric_smul G G means that G has a left-invariant metric while has_isometric_smul Gᵐᵒᵖ G means that G has a right-invariant metric. For a commutative group, these two notions are equivalent. A group with a right-invariant metric can be also represented as a normed_group.

source
@[class]
structure has_isometric_vadd (M : Type u) (X : Type w) [pseudo_emetric_space X] [has_vadd M X] :
Prop

An additive action is isometric if each map x ↦ c +ᵥ x is an isometry.

Instances of this typeclass
source
@[class]
structure has_isometric_smul (M : Type u) (X : Type w) [pseudo_emetric_space X] [has_smul M X] :
Prop

A multiplicative action is isometric if each map x ↦ c • x is an isometry.

Instances of this typeclass
source
@[protected, instance]
def has_isometric_vadd.to_has_continuous_const_vadd (M : Type u) (X : Type w) [pseudo_emetric_space X] [has_vadd M X] [has_isometric_vadd M X] :
has_continuous_const_vadd M X
source
@[protected, instance]
def has_isometric_smul.to_has_continuous_const_smul (M : Type u) (X : Type w) [pseudo_emetric_space X] [has_smul M X] [has_isometric_smul M X] :
has_continuous_const_smul M X
source
@[protected, instance]
def has_isometric_smul.opposite_of_comm (M : Type u) (X : Type w) [pseudo_emetric_space X] [has_smul M X] [has_smul Mᵐᵒᵖ X] [is_central_scalar M X] [has_isometric_smul M X] :
has_isometric_smul Mᵐᵒᵖ X
source
@[protected, instance]
def has_isometric_vadd.opposite_of_comm (M : Type u) (X : Type w) [pseudo_emetric_space X] [has_vadd M X] [has_vadd Mᵃᵒᵖ X] [is_central_vadd M X] [has_isometric_vadd M X] :
has_isometric_vadd Mᵃᵒᵖ X
source
@[simp]
theorem edist_vadd_left {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_vadd M X] [has_isometric_vadd M X] (c : M) (x y : X) :
has_edist.edist (c +ᵥ x) (c +ᵥ y) = has_edist.edist x y
source
@[simp]
theorem edist_smul_left {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_smul M X] [has_isometric_smul M X] (c : M) (x y : X) :
has_edist.edist (c • x) (c • y) = has_edist.edist x y
source
@[simp]
theorem ediam_smul {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_smul M X] [has_isometric_smul M X] (c : M) (s : set X) :
emetric.diam (c • s) = emetric.diam s
source
@[simp]
theorem ediam_vadd {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_vadd M X] [has_isometric_vadd M X] (c : M) (s : set X) :
emetric.diam (c +ᵥ s) = emetric.diam s
source
theorem isometry_add_left {M : Type u} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd M M] (a : M) :
isometry (has_add.add a)
source
theorem isometry_mul_left {M : Type u} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul M M] (a : M) :
isometry (has_mul.mul a)
source
@[simp]
theorem edist_mul_left {M : Type u} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul M M] (a b c : M) :
has_edist.edist (a * b) (a * c) = has_edist.edist b c
source
@[simp]
theorem edist_add_left {M : Type u} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd M M] (a b c : M) :
has_edist.edist (a + b) (a + c) = has_edist.edist b c
source
theorem isometry_add_right {M : Type u} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd Mᵃᵒᵖ M] (a : M) :
isometry (λ (x : M), x + a)
source
theorem isometry_mul_right {M : Type u} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul Mᵐᵒᵖ M] (a : M) :
isometry (λ (x : M), x * a)
source
@[simp]
theorem edist_add_right {M : Type u} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd Mᵃᵒᵖ M] (a b c : M) :
has_edist.edist (a + c) (b + c) = has_edist.edist a b
source
@[simp]
theorem edist_mul_right {M : Type u} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul Mᵐᵒᵖ M] (a b c : M) :
has_edist.edist (a * c) (b * c) = has_edist.edist a b
source
@[simp]
theorem edist_div_right {M : Type u} [div_inv_monoid M] [pseudo_emetric_space M] [has_isometric_smul Mᵐᵒᵖ M] (a b c : M) :
has_edist.edist (a / c) (b / c) = has_edist.edist a b
source
@[simp]
theorem edist_sub_right {M : Type u} [sub_neg_monoid M] [pseudo_emetric_space M] [has_isometric_vadd Mᵃᵒᵖ M] (a b c : M) :
has_edist.edist (a - c) (b - c) = has_edist.edist a b
source
@[simp]
theorem edist_inv_inv {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (a b : G) :
has_edist.edist a⁻¹ b⁻¹ = has_edist.edist a b
source
@[simp]
theorem edist_neg_neg {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (a b : G) :
has_edist.edist (-a) (-b) = has_edist.edist a b
source
theorem isometry_inv {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] :
isometry has_inv.inv
source
theorem isometry_neg {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] :
isometry has_neg.neg
source
theorem edist_inv {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (x y : G) :
has_edist.edist x⁻¹ y = has_edist.edist x y⁻¹
source
theorem edist_neg {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (x y : G) :
has_edist.edist (-x) y = has_edist.edist x (-y)
source
@[simp]
theorem edist_div_left {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (a b c : G) :
has_edist.edist (a / b) (a / c) = has_edist.edist b c
source
@[simp]
theorem edist_sub_left {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (a b c : G) :
has_edist.edist (a - b) (a - c) = has_edist.edist b c
source
@[simp]
theorem isometry_equiv.const_vadd_apply {G : Type v} {X : Type w} [pseudo_emetric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) :
⇑(isometry_equiv.const_vadd c) x = c +ᵥ x
source
@[simp]
theorem isometry_equiv.const_smul_apply {G : Type v} {X : Type w} [pseudo_emetric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) :
⇑(isometry_equiv.const_smul c) x = c • x
source
def isometry_equiv.const_vadd {G : Type v} {X : Type w} [pseudo_emetric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) :
X ≃ᵢ X

If an additive group G acts on X by isometries, then isometry_equiv.const_vadd is the isometry of X given by addition of a constant element of the group.

Equations
source
@[simp]
theorem isometry_equiv.const_vadd_to_equiv {G : Type v} {X : Type w} [pseudo_emetric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) :
(isometry_equiv.const_vadd c).to_equiv = add_action.to_perm c
source
def isometry_equiv.const_smul {G : Type v} {X : Type w} [pseudo_emetric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) :
X ≃ᵢ X

If a group G acts on X by isometries, then isometry_equiv.const_smul is the isometry of X given by multiplication of a constant element of the group.

Equations
source
@[simp]
theorem isometry_equiv.const_smul_to_equiv {G : Type v} {X : Type w} [pseudo_emetric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) :
(isometry_equiv.const_smul c).to_equiv = mul_action.to_perm c
source
@[simp]
theorem isometry_equiv.const_smul_symm {G : Type v} {X : Type w} [pseudo_emetric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) :
(isometry_equiv.const_smul c).symm = isometry_equiv.const_smul c⁻¹
source
@[simp]
theorem isometry_equiv.const_vadd_symm {G : Type v} {X : Type w} [pseudo_emetric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) :
(isometry_equiv.const_vadd c).symm = isometry_equiv.const_vadd (-c)
source
def isometry_equiv.add_left {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] (c : G) :
G ≃ᵢ G

Addition y ↦ x + y as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.mul_left_apply {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] (c x : G) :
⇑(isometry_equiv.mul_left c) x = c * x
source
@[simp]
theorem isometry_equiv.add_left_to_equiv {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] (c : G) :
(isometry_equiv.add_left c).to_equiv = equiv.add_left c
source
@[simp]
theorem isometry_equiv.add_left_apply {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] (c x : G) :
⇑(isometry_equiv.add_left c) x = c + x
source
def isometry_equiv.mul_left {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] (c : G) :
G ≃ᵢ G

Multiplication y ↦ x * y as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.mul_left_to_equiv {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] (c : G) :
(isometry_equiv.mul_left c).to_equiv = equiv.mul_left c
source
@[simp]
theorem isometry_equiv.add_left_symm {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] (x : G) :
(isometry_equiv.add_left x).symm = isometry_equiv.add_left (-x)
source
@[simp]
theorem isometry_equiv.mul_left_symm {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] (x : G) :
(isometry_equiv.mul_left x).symm = isometry_equiv.mul_left x⁻¹
source
@[simp]
theorem isometry_equiv.mul_right_to_equiv {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (c : G) :
(isometry_equiv.mul_right c).to_equiv = equiv.mul_right c
source
@[simp]
theorem isometry_equiv.add_right_apply {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (c x : G) :
⇑(isometry_equiv.add_right c) x = x + c
source
def isometry_equiv.mul_right {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (c : G) :
G ≃ᵢ G

Multiplication y ↦ y * x as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.mul_right_apply {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (c x : G) :
⇑(isometry_equiv.mul_right c) x = x * c
source
def isometry_equiv.add_right {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (c : G) :
G ≃ᵢ G

Addition y ↦ y + x as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.add_right_to_equiv {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (c : G) :
(isometry_equiv.add_right c).to_equiv = equiv.add_right c
source
@[simp]
theorem isometry_equiv.add_right_symm {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (x : G) :
(isometry_equiv.add_right x).symm = isometry_equiv.add_right (-x)
source
@[simp]
theorem isometry_equiv.mul_right_symm {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (x : G) :
(isometry_equiv.mul_right x).symm = isometry_equiv.mul_right x⁻¹
source
def isometry_equiv.div_right {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (c : G) :
G ≃ᵢ G

Division y ↦ y / x as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.sub_right_to_equiv {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (c : G) :
(isometry_equiv.sub_right c).to_equiv = equiv.sub_right c
source
@[simp]
theorem isometry_equiv.div_right_to_equiv {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (c : G) :
(isometry_equiv.div_right c).to_equiv = equiv.div_right c
source
def isometry_equiv.sub_right {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (c : G) :
G ≃ᵢ G

Subtraction y ↦ y - x as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.sub_right_apply {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (c b : G) :
⇑(isometry_equiv.sub_right c) b = b - c
source
@[simp]
theorem isometry_equiv.div_right_apply {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (c b : G) :
⇑(isometry_equiv.div_right c) b = b / c
source
@[simp]
theorem isometry_equiv.sub_right_symm {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (c : G) :
(isometry_equiv.sub_right c).symm = isometry_equiv.add_right c
source
@[simp]
theorem isometry_equiv.div_right_symm {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (c : G) :
(isometry_equiv.div_right c).symm = isometry_equiv.mul_right c
source
@[simp]
theorem isometry_equiv.sub_left_apply {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (c b : G) :
⇑(isometry_equiv.sub_left c) b = c - b
source
@[simp]
theorem isometry_equiv.sub_left_to_equiv {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (c : G) :
(isometry_equiv.sub_left c).to_equiv = equiv.sub_left c
source
def isometry_equiv.sub_left {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (c : G) :
G ≃ᵢ G

Subtraction y ↦ x - y as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.sub_left_symm_apply {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (c b : G) :
⇑((isometry_equiv.sub_left c).symm) b = -b + c
source
def isometry_equiv.div_left {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (c : G) :
G ≃ᵢ G

Division y ↦ x / y as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.div_left_to_equiv {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (c : G) :
(isometry_equiv.div_left c).to_equiv = equiv.div_left c
source
@[simp]
theorem isometry_equiv.div_left_apply {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (c b : G) :
⇑(isometry_equiv.div_left c) b = c / b
source
@[simp]
theorem isometry_equiv.div_left_symm_apply {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (c b : G) :
⇑((isometry_equiv.div_left c).symm) b = b⁻¹ * c
source
@[simp]
theorem isometry_equiv.neg_apply (G : Type v) [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (ᾰ : G) :
⇑(isometry_equiv.neg G) ᾰ = -ᾰ
source
def isometry_equiv.neg (G : Type v) [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] :
G ≃ᵢ G

Negation x ↦ -x as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.inv_apply (G : Type v) [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (ᾰ : G) :
⇑(isometry_equiv.inv G) ᾰ = ᾰ⁻¹
source
@[simp]
theorem isometry_equiv.inv_to_equiv (G : Type v) [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] :
(isometry_equiv.inv G).to_equiv = equiv.inv G
source
def isometry_equiv.inv (G : Type v) [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] :
G ≃ᵢ G

Inversion x ↦ x⁻¹ as an isometry_equiv.

Equations
source
@[simp]
theorem isometry_equiv.neg_to_equiv (G : Type v) [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] :
(isometry_equiv.neg G).to_equiv = equiv.neg G
source
@[simp]
theorem isometry_equiv.neg_symm (G : Type v) [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] :
(isometry_equiv.neg G).symm = isometry_equiv.neg G
source
@[simp]
theorem isometry_equiv.inv_symm (G : Type v) [group G] [pseudo_emetric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] :
(isometry_equiv.inv G).symm = isometry_equiv.inv G
source
@[simp]
theorem emetric.smul_ball {G : Type v} {X : Type w} [pseudo_emetric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ennreal) :
c • emetric.ball x r = emetric.ball (c • x) r
source
@[simp]
theorem emetric.vadd_ball {G : Type v} {X : Type w} [pseudo_emetric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ennreal) :
c +ᵥ emetric.ball x r = emetric.ball (c +ᵥ x) r
source
@[simp]
theorem emetric.preimage_vadd_ball {G : Type v} {X : Type w} [pseudo_emetric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ennreal) :
has_vadd.vadd c ⁻¹' emetric.ball x r = emetric.ball (-c +ᵥ x) r
source
@[simp]
theorem emetric.preimage_smul_ball {G : Type v} {X : Type w} [pseudo_emetric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ennreal) :
has_smul.smul c ⁻¹' emetric.ball x r = emetric.ball (c⁻¹ • x) r
source
@[simp]
theorem emetric.vadd_closed_ball {G : Type v} {X : Type w} [pseudo_emetric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ennreal) :
c +ᵥ emetric.closed_ball x r = emetric.closed_ball (c +ᵥ x) r
source
@[simp]
theorem emetric.smul_closed_ball {G : Type v} {X : Type w} [pseudo_emetric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ennreal) :
c • emetric.closed_ball x r = emetric.closed_ball (c • x) r
source
@[simp]
theorem emetric.preimage_smul_closed_ball {G : Type v} {X : Type w} [pseudo_emetric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ennreal) :
has_smul.smul c ⁻¹' emetric.closed_ball x r = emetric.closed_ball (c⁻¹ • x) r
source
@[simp]
theorem emetric.preimage_vadd_closed_ball {G : Type v} {X : Type w} [pseudo_emetric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ennreal) :
has_vadd.vadd c ⁻¹' emetric.closed_ball x r = emetric.closed_ball (-c +ᵥ x) r
source
@[simp]
theorem emetric.preimage_mul_left_ball {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] (a b : G) (r : ennreal) :
has_mul.mul a ⁻¹' emetric.ball b r = emetric.ball (a⁻¹ * b) r
source
@[simp]
theorem emetric.preimage_add_left_ball {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] (a b : G) (r : ennreal) :
has_add.add a ⁻¹' emetric.ball b r = emetric.ball (-a + b) r
source
@[simp]
theorem emetric.preimage_add_right_ball {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (a b : G) (r : ennreal) :
(λ (x : G), x + a) ⁻¹' emetric.ball b r = emetric.ball (b - a) r
source
@[simp]
theorem emetric.preimage_mul_right_ball {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (a b : G) (r : ennreal) :
(λ (x : G), x * a) ⁻¹' emetric.ball b r = emetric.ball (b / a) r
source
@[simp]
theorem emetric.preimage_add_left_closed_ball {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd G G] (a b : G) (r : ennreal) :
has_add.add a ⁻¹' emetric.closed_ball b r = emetric.closed_ball (-a + b) r
source
@[simp]
theorem emetric.preimage_mul_left_closed_ball {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul G G] (a b : G) (r : ennreal) :
has_mul.mul a ⁻¹' emetric.closed_ball b r = emetric.closed_ball (a⁻¹ * b) r
source
@[simp]
theorem emetric.preimage_add_right_closed_ball {G : Type v} [add_group G] [pseudo_emetric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (a b : G) (r : ennreal) :
(λ (x : G), x + a) ⁻¹' emetric.closed_ball b r = emetric.closed_ball (b - a) r
source
@[simp]
theorem emetric.preimage_mul_right_closed_ball {G : Type v} [group G] [pseudo_emetric_space G] [has_isometric_smul Gᵐᵒᵖ G] (a b : G) (r : ennreal) :
(λ (x : G), x * a) ⁻¹' emetric.closed_ball b r = emetric.closed_ball (b / a) r
source
@[simp]
theorem dist_smul {M : Type u} {X : Type w} [pseudo_metric_space X] [has_smul M X] [has_isometric_smul M X] (c : M) (x y : X) :
has_dist.dist (c • x) (c • y) = has_dist.dist x y
source
@[simp]
theorem dist_vadd {M : Type u} {X : Type w} [pseudo_metric_space X] [has_vadd M X] [has_isometric_vadd M X] (c : M) (x y : X) :
has_dist.dist (c +ᵥ x) (c +ᵥ y) = has_dist.dist x y
source
@[simp]
theorem nndist_smul {M : Type u} {X : Type w} [pseudo_metric_space X] [has_smul M X] [has_isometric_smul M X] (c : M) (x y : X) :
has_nndist.nndist (c • x) (c • y) = has_nndist.nndist x y
source
@[simp]
theorem nndist_vadd {M : Type u} {X : Type w} [pseudo_metric_space X] [has_vadd M X] [has_isometric_vadd M X] (c : M) (x y : X) :
has_nndist.nndist (c +ᵥ x) (c +ᵥ y) = has_nndist.nndist x y
source
@[simp]
theorem diam_vadd {M : Type u} {X : Type w} [pseudo_metric_space X] [has_vadd M X] [has_isometric_vadd M X] (c : M) (s : set X) :
metric.diam (c +ᵥ s) = metric.diam s
source
@[simp]
theorem diam_smul {M : Type u} {X : Type w} [pseudo_metric_space X] [has_smul M X] [has_isometric_smul M X] (c : M) (s : set X) :
metric.diam (c • s) = metric.diam s
source
@[simp]
theorem dist_add_left {M : Type u} [pseudo_metric_space M] [has_add M] [has_isometric_vadd M M] (a b c : M) :
has_dist.dist (a + b) (a + c) = has_dist.dist b c
source
@[simp]
theorem dist_mul_left {M : Type u} [pseudo_metric_space M] [has_mul M] [has_isometric_smul M M] (a b c : M) :
has_dist.dist (a * b) (a * c) = has_dist.dist b c
source
@[simp]
theorem nndist_mul_left {M : Type u} [pseudo_metric_space M] [has_mul M] [has_isometric_smul M M] (a b c : M) :
has_nndist.nndist (a * b) (a * c) = has_nndist.nndist b c
source
@[simp]
theorem nndist_add_left {M : Type u} [pseudo_metric_space M] [has_add M] [has_isometric_vadd M M] (a b c : M) :
has_nndist.nndist (a + b) (a + c) = has_nndist.nndist b c
source
@[simp]
theorem dist_add_right {M : Type u} [has_add M] [pseudo_metric_space M] [has_isometric_vadd Mᵃᵒᵖ M] (a b c : M) :
has_dist.dist (a + c) (b + c) = has_dist.dist a b
source
@[simp]
theorem dist_mul_right {M : Type u} [has_mul M] [pseudo_metric_space M] [has_isometric_smul Mᵐᵒᵖ M] (a b c : M) :
has_dist.dist (a * c) (b * c) = has_dist.dist a b
source
@[simp]
theorem nndist_add_right {M : Type u} [pseudo_metric_space M] [has_add M] [has_isometric_vadd Mᵃᵒᵖ M] (a b c : M) :
has_nndist.nndist (a + c) (b + c) = has_nndist.nndist a b
source
@[simp]
theorem nndist_mul_right {M : Type u} [pseudo_metric_space M] [has_mul M] [has_isometric_smul Mᵐᵒᵖ M] (a b c : M) :
has_nndist.nndist (a * c) (b * c) = has_nndist.nndist a b
source
@[simp]
theorem dist_div_right {M : Type u} [div_inv_monoid M] [pseudo_metric_space M] [has_isometric_smul Mᵐᵒᵖ M] (a b c : M) :
has_dist.dist (a / c) (b / c) = has_dist.dist a b
source
@[simp]
theorem dist_sub_right {M : Type u} [sub_neg_monoid M] [pseudo_metric_space M] [has_isometric_vadd Mᵃᵒᵖ M] (a b c : M) :
has_dist.dist (a - c) (b - c) = has_dist.dist a b
source
@[simp]
theorem nndist_sub_right {M : Type u} [sub_neg_monoid M] [pseudo_metric_space M] [has_isometric_vadd Mᵃᵒᵖ M] (a b c : M) :
has_nndist.nndist (a - c) (b - c) = has_nndist.nndist a b
source
@[simp]
theorem nndist_div_right {M : Type u} [div_inv_monoid M] [pseudo_metric_space M] [has_isometric_smul Mᵐᵒᵖ M] (a b c : M) :
has_nndist.nndist (a / c) (b / c) = has_nndist.nndist a b
source
@[simp]
theorem dist_neg_neg {G : Type v} [add_group G] [pseudo_metric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (a b : G) :
has_dist.dist (-a) (-b) = has_dist.dist a b
source
@[simp]
theorem dist_inv_inv {G : Type v} [group G] [pseudo_metric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (a b : G) :
has_dist.dist a⁻¹ b⁻¹ = has_dist.dist a b
source
@[simp]
theorem nndist_neg_neg {G : Type v} [add_group G] [pseudo_metric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (a b : G) :
has_nndist.nndist (-a) (-b) = has_nndist.nndist a b
source
@[simp]
theorem nndist_inv_inv {G : Type v} [group G] [pseudo_metric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (a b : G) :
has_nndist.nndist a⁻¹ b⁻¹ = has_nndist.nndist a b
source
@[simp]
theorem dist_div_left {G : Type v} [group G] [pseudo_metric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (a b c : G) :
has_dist.dist (a / b) (a / c) = has_dist.dist b c
source
@[simp]
theorem dist_sub_left {G : Type v} [add_group G] [pseudo_metric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (a b c : G) :
has_dist.dist (a - b) (a - c) = has_dist.dist b c
source
@[simp]
theorem nndist_sub_left {G : Type v} [add_group G] [pseudo_metric_space G] [has_isometric_vadd G G] [has_isometric_vadd Gᵃᵒᵖ G] (a b c : G) :
has_nndist.nndist (a - b) (a - c) = has_nndist.nndist b c
source
@[simp]
theorem nndist_div_left {G : Type v} [group G] [pseudo_metric_space G] [has_isometric_smul G G] [has_isometric_smul Gᵐᵒᵖ G] (a b c : G) :
has_nndist.nndist (a / b) (a / c) = has_nndist.nndist b c
source
@[simp]
theorem metric.vadd_ball {G : Type v} {X : Type w} [pseudo_metric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ℝ) :
c +ᵥ metric.ball x r = metric.ball (c +ᵥ x) r
source
@[simp]
theorem metric.smul_ball {G : Type v} {X : Type w} [pseudo_metric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ℝ) :
c • metric.ball x r = metric.ball (c • x) r
source
@[simp]
theorem metric.preimage_vadd_ball {G : Type v} {X : Type w} [pseudo_metric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ℝ) :
has_vadd.vadd c ⁻¹' metric.ball x r = metric.ball (-c +ᵥ x) r
source
@[simp]
theorem metric.preimage_smul_ball {G : Type v} {X : Type w} [pseudo_metric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ℝ) :
has_smul.smul c ⁻¹' metric.ball x r = metric.ball (c⁻¹ • x) r
source
@[simp]
theorem metric.smul_closed_ball {G : Type v} {X : Type w} [pseudo_metric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ℝ) :
c • metric.closed_ball x r = metric.closed_ball (c • x) r
source
@[simp]
theorem metric.vadd_closed_ball {G : Type v} {X : Type w} [pseudo_metric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ℝ) :
c +ᵥ metric.closed_ball x r = metric.closed_ball (c +ᵥ x) r
source
@[simp]
theorem metric.preimage_smul_closed_ball {G : Type v} {X : Type w} [pseudo_metric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ℝ) :
has_smul.smul c ⁻¹' metric.closed_ball x r = metric.closed_ball (c⁻¹ • x) r
source
@[simp]
theorem metric.preimage_vadd_closed_ball {G : Type v} {X : Type w} [pseudo_metric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ℝ) :
has_vadd.vadd c ⁻¹' metric.closed_ball x r = metric.closed_ball (-c +ᵥ x) r
source
@[simp]
theorem metric.smul_sphere {G : Type v} {X : Type w} [pseudo_metric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ℝ) :
c • metric.sphere x r = metric.sphere (c • x) r
source
@[simp]
theorem metric.vadd_sphere {G : Type v} {X : Type w} [pseudo_metric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ℝ) :
c +ᵥ metric.sphere x r = metric.sphere (c +ᵥ x) r
source
@[simp]
theorem metric.preimage_vadd_sphere {G : Type v} {X : Type w} [pseudo_metric_space X] [add_group G] [add_action G X] [has_isometric_vadd G X] (c : G) (x : X) (r : ℝ) :
has_vadd.vadd c ⁻¹' metric.sphere x r = metric.sphere (-c +ᵥ x) r
source
@[simp]
theorem metric.preimage_smul_sphere {G : Type v} {X : Type w} [pseudo_metric_space X] [group G] [mul_action G X] [has_isometric_smul G X] (c : G) (x : X) (r : ℝ) :
has_smul.smul c ⁻¹' metric.sphere x r = metric.sphere (c⁻¹ • x) r
source
@[simp]
theorem metric.preimage_add_left_ball {G : Type v} [add_group G] [pseudo_metric_space G] [has_isometric_vadd G G] (a b : G) (r : ℝ) :
has_add.add a ⁻¹' metric.ball b r = metric.ball (-a + b) r
source
@[simp]
theorem metric.preimage_mul_left_ball {G : Type v} [group G] [pseudo_metric_space G] [has_isometric_smul G G] (a b : G) (r : ℝ) :
has_mul.mul a ⁻¹' metric.ball b r = metric.ball (a⁻¹ * b) r
source
@[simp]
theorem metric.preimage_mul_right_ball {G : Type v} [group G] [pseudo_metric_space G] [has_isometric_smul Gᵐᵒᵖ G] (a b : G) (r : ℝ) :
(λ (x : G), x * a) ⁻¹' metric.ball b r = metric.ball (b / a) r
source
@[simp]
theorem metric.preimage_add_right_ball {G : Type v} [add_group G] [pseudo_metric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (a b : G) (r : ℝ) :
(λ (x : G), x + a) ⁻¹' metric.ball b r = metric.ball (b - a) r
source
@[simp]
theorem metric.preimage_mul_left_closed_ball {G : Type v} [group G] [pseudo_metric_space G] [has_isometric_smul G G] (a b : G) (r : ℝ) :
has_mul.mul a ⁻¹' metric.closed_ball b r = metric.closed_ball (a⁻¹ * b) r
source
@[simp]
theorem metric.preimage_add_left_closed_ball {G : Type v} [add_group G] [pseudo_metric_space G] [has_isometric_vadd G G] (a b : G) (r : ℝ) :
has_add.add a ⁻¹' metric.closed_ball b r = metric.closed_ball (-a + b) r
source
@[simp]
theorem metric.preimage_add_right_closed_ball {G : Type v} [add_group G] [pseudo_metric_space G] [has_isometric_vadd Gᵃᵒᵖ G] (a b : G) (r : ℝ) :
(λ (x : G), x + a) ⁻¹' metric.closed_ball b r = metric.closed_ball (b - a) r
source
@[simp]
theorem metric.preimage_mul_right_closed_ball {G : Type v} [group G] [pseudo_metric_space G] [has_isometric_smul Gᵐᵒᵖ G] (a b : G) (r : ℝ) :
(λ (x : G), x * a) ⁻¹' metric.closed_ball b r = metric.closed_ball (b / a) r
source
@[protected, instance]
def prod.has_isometric_smul {M : Type u} {X : Type w} {Y : Type u_1} [pseudo_emetric_space X] [pseudo_emetric_space Y] [has_smul M X] [has_isometric_smul M X] [has_smul M Y] [has_isometric_smul M Y] :
has_isometric_smul M (X × Y)
source
@[protected, instance]
def prod.has_isometric_vadd {M : Type u} {X : Type w} {Y : Type u_1} [pseudo_emetric_space X] [pseudo_emetric_space Y] [has_vadd M X] [has_isometric_vadd M X] [has_vadd M Y] [has_isometric_vadd M Y] :
has_isometric_vadd M (X × Y)
source
@[protected, instance]
def prod.has_isometric_vadd' {M : Type u} {N : Type u_1} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd M M] [has_add N] [pseudo_emetric_space N] [has_isometric_vadd N N] :
has_isometric_vadd (M × N) (M × N)
source
@[protected, instance]
def prod.has_isometric_smul' {M : Type u} {N : Type u_1} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul M M] [has_mul N] [pseudo_emetric_space N] [has_isometric_smul N N] :
has_isometric_smul (M × N) (M × N)
source
@[protected, instance]
def prod.has_isometric_smul'' {M : Type u} {N : Type u_1} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul Mᵐᵒᵖ M] [has_mul N] [pseudo_emetric_space N] [has_isometric_smul Nᵐᵒᵖ N] :
has_isometric_smul (M × N)ᵐᵒᵖ (M × N)
source
@[protected, instance]
def prod.has_isometric_vadd'' {M : Type u} {N : Type u_1} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd Mᵃᵒᵖ M] [has_add N] [pseudo_emetric_space N] [has_isometric_vadd Nᵃᵒᵖ N] :
has_isometric_vadd (M × N)ᵃᵒᵖ (M × N)
source
@[protected, instance]
def add_units.has_isometric_vadd {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_vadd M X] [has_isometric_vadd M X] [add_monoid M] :
has_isometric_vadd (add_units M) X
source
@[protected, instance]
def units.has_isometric_smul {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_smul M X] [has_isometric_smul M X] [monoid M] :
has_isometric_smul Mˣ X
source
@[protected, instance]
def mul_opposite.has_isometric_smul {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_smul M X] [has_isometric_smul M X] :
has_isometric_smul M Xᵐᵒᵖ
source
@[protected, instance]
def add_opposite.has_isometric_vadd {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_vadd M X] [has_isometric_vadd M X] :
has_isometric_vadd M Xᵃᵒᵖ
source
@[protected, instance]
def ulift.has_isometric_vadd {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_vadd M X] [has_isometric_vadd M X] :
has_isometric_vadd (ulift M) X
source
@[protected, instance]
def ulift.has_isometric_smul {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_smul M X] [has_isometric_smul M X] :
has_isometric_smul (ulift M) X
source
@[protected, instance]
def ulift.has_isometric_vadd' {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_vadd M X] [has_isometric_vadd M X] :
has_isometric_vadd M (ulift X)
source
@[protected, instance]
def ulift.has_isometric_smul' {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_smul M X] [has_isometric_smul M X] :
has_isometric_smul M (ulift X)
source
@[protected, instance]
def pi.has_isometric_smul {M : Type u} {ι : Type u_1} {X : ι → Type u_2} [fintype ι] [Π (i : ι), has_smul M (X i)] [Π (i : ι), pseudo_emetric_space (X i)] [∀ (i : ι), has_isometric_smul M (X i)] :
has_isometric_smul M (Π (i : ι), X i)
source
@[protected, instance]
def pi.has_isometric_vadd {M : Type u} {ι : Type u_1} {X : ι → Type u_2} [fintype ι] [Π (i : ι), has_vadd M (X i)] [Π (i : ι), pseudo_emetric_space (X i)] [∀ (i : ι), has_isometric_vadd M (X i)] :
has_isometric_vadd M (Π (i : ι), X i)
source
@[protected, instance]
def pi.has_isometric_vadd' {ι : Type u_1} {M : ι → Type u_2} {X : ι → Type u_3} [fintype ι] [Π (i : ι), has_vadd (M i) (X i)] [Π (i : ι), pseudo_emetric_space (X i)] [∀ (i : ι), has_isometric_vadd (M i) (X i)] :
has_isometric_vadd (Π (i : ι), M i) (Π (i : ι), X i)
source
@[protected, instance]
def pi.has_isometric_smul' {ι : Type u_1} {M : ι → Type u_2} {X : ι → Type u_3} [fintype ι] [Π (i : ι), has_smul (M i) (X i)] [Π (i : ι), pseudo_emetric_space (X i)] [∀ (i : ι), has_isometric_smul (M i) (X i)] :
has_isometric_smul (Π (i : ι), M i) (Π (i : ι), X i)
source
@[protected, instance]
def pi.has_isometric_smul'' {ι : Type u_1} {M : ι → Type u_2} [fintype ι] [Π (i : ι), has_mul (M i)] [Π (i : ι), pseudo_emetric_space (M i)] [∀ (i : ι), has_isometric_smul (M i)ᵐᵒᵖ (M i)] :
has_isometric_smul (Π (i : ι), M i)ᵐᵒᵖ (Π (i : ι), M i)
source
@[protected, instance]
def pi.has_isometric_vadd'' {ι : Type u_1} {M : ι → Type u_2} [fintype ι] [Π (i : ι), has_add (M i)] [Π (i : ι), pseudo_emetric_space (M i)] [∀ (i : ι), has_isometric_vadd (M i)ᵃᵒᵖ (M i)] :
has_isometric_vadd (Π (i : ι), M i)ᵃᵒᵖ (Π (i : ι), M i)
source
@[protected, instance]
def additive.has_isometric_vadd {M : Type u} {X : Type w} [pseudo_emetric_space X] [has_smul M X] [has_isometric_smul M X] :
has_isometric_vadd (additive M) X
source
@[protected, instance]
def additive.has_isometric_vadd' {M : Type u} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul M M] :
has_isometric_vadd (additive M) (additive M)
source
@[protected, instance]
def additive.has_isometric_vadd'' {M : Type u} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul Mᵐᵒᵖ M] :
has_isometric_vadd (additive M)ᵃᵒᵖ (additive M)
source
@[protected, instance]
def multiplicative.has_isometric_smul {M : Type u_1} {X : Type u_2} [has_vadd M X] [pseudo_emetric_space X] [has_isometric_vadd M X] :
has_isometric_smul (multiplicative M) X
source
@[protected, instance]
def multiplicative.has_isometric_smul' {M : Type u} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd M M] :
has_isometric_smul (multiplicative M) (multiplicative M)
source
@[protected, instance]
def multiplicative.has_isometric_vadd'' {M : Type u} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd Mᵃᵒᵖ M] :
has_isometric_smul (multiplicative M)ᵐᵒᵖ (multiplicative M)