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.

@[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) :
@[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) :
@[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) :
@[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) :
@[simp]
theorem edist_mul_left {M : Type u} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul M M] (a b c : M) :
@[simp]
theorem edist_add_left {M : Type u} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd M M] (a b c : M) :
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)
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)
@[simp]
theorem edist_add_right {M : Type u} [has_add M] [pseudo_emetric_space M] [has_isometric_vadd Mᵃᵒᵖ M] (a b c : M) :
@[simp]
theorem edist_mul_right {M : Type u} [has_mul M] [pseudo_emetric_space M] [has_isometric_smul Mᵐᵒᵖ M] (a b c : M) :
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[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) :
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
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

Multiplication y ↦ x * y as an isometry_equiv.

Equations
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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
@[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
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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
@[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
@[simp]
theorem nndist_mul_left {M : Type u} [pseudo_metric_space M] [has_mul M] [has_isometric_smul M M] (a b c : M) :
@[simp]
theorem nndist_add_left {M : Type u} [pseudo_metric_space M] [has_add M] [has_isometric_vadd M M] (a b c : M) :
@[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
@[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
@[simp]
@[simp]
@[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
@[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
@[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
@[simp]
@[simp]
@[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 : ) :
@[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 : ) :
@[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 : ) :
@[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 : ) :
@[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 : ) :
@[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 : ) :
@[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 : ) :
@[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 : ) :
@[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 : ) :
@[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 : ) :
@[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
@[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
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[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)
@[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)
@[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)
@[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)
@[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)
@[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)
@[protected, instance]