Theorems · Theorem · geometry

Similar.comp_left

∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃] {F : Type u_6}
  [inst_3 : FunLike F P₁ P₃] [DilationClass F P₁ P₃] (f : F), Similar v₁ v₂ → Similar (⇑f ∘ v₁) v₂

Defined in

Mathlib.Topology.MetricSpace.Similarity

Cited by

3 results in Mathlib

Foundations

Depth 151 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpacePseudoEMetricSpacePseudoEMetricSpaceFunLikeDilationClass