Mathlib Map

Theorems Ā· Definition Ā· geometry

AffineIsometry.comp

{š•œ : Type u_1} ā†’
  {V : Type u_2} ā†’
    {Vā‚‚ : Type u_5} ā†’
      {Vā‚ƒ : Type u_6} ā†’
        {P : Type u_10} ā†’
          {Pā‚‚ : Type u_11} ā†’
            {Pā‚ƒ : Type u_12} ā†’
              [inst : NormedField š•œ] ā†’
                [inst_1 : SeminormedAddCommGroup V] ā†’
                  [inst_2 : NormedSpace š•œ V] ā†’
                    [inst_3 : PseudoMetricSpace P] ā†’
                      [inst_4 : NormedAddTorsor V P] ā†’
                        [inst_5 : SeminormedAddCommGroup Vā‚‚] ā†’
                          [inst_6 : NormedSpace š•œ Vā‚‚] ā†’
                            [inst_7 : PseudoMetricSpace Pā‚‚] ā†’
                              [inst_8 : NormedAddTorsor Vā‚‚ Pā‚‚] ā†’
                                [inst_9 : SeminormedAddCommGroup Vā‚ƒ] ā†’
                                  [inst_10 : NormedSpace š•œ Vā‚ƒ] ā†’
                                    [inst_11 : PseudoMetricSpace Pā‚ƒ] ā†’
                                      [inst_12 : NormedAddTorsor Vā‚ƒ Pā‚ƒ] ā†’ (Pā‚‚ ā†’įµƒā±[š•œ] Pā‚ƒ) ā†’ (P ā†’įµƒā±[š•œ] Pā‚‚) ā†’ P ā†’įµƒā±[š•œ] Pā‚ƒ

Composition of affine isometries.

Defined in
Mathlib.Analysis.Normed.Affine.Isometry
Cited by
4 results in Mathlib
Foundations
Depth 49 from the axioms Ā· uses propext, Quot.sound
Assumes
NormedFieldSeminormedAddCommGroupNormedSpacePseudoMetricSpaceNormedAddTorsorSeminormedAddCommGroupNormedSpacePseudoMetricSpaceNormedAddTorsorSeminormedAddCommGroupNormedSpacePseudoMetricSpaceNormedAddTorsor
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AffineIsometry.id_comp Ā· cited by 0AffineIsometry.id_compAffineIsometry.coe_comp Ā· cited by 0AffineIsometry.coe_compAffineIsometry.comp_assoc Ā· cited by 0AffineIsometry.comp_assocAffineIsometry.comp_id Ā· cited by 0AffineIsometry.comp_idNormedSpace Ā· cited by 12499NormedSpaceSeminormedAddCommGroup Ā· cited by 2671SeminormedAddCommGroupPseudoMetricSpace Ā· cited by 1550PseudoMetricSpaceNormedAddTorsor Ā· cited by 1325NormedAddTorsorNormedField Ā· cited by 1084NormedFieldAffineIsometry Ā· cited by 79AffineIsometryAffineIsometry.toAffineMap Ā· cited by 42AffineIsometry.toAffineMapAffineMap.comp Ā· cited by 20AffineMap.compAffineIsometry.compCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.