Theorems · Theorem · general topology

Congruent.comp_dilation

∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {P₃ : Type u_5} {P₄ : Type u_6} {v₁ : ι → P₁} {v₂ : ι → P₂}
  [inst : PseudoEMetricSpace P₁] [inst_1 : PseudoEMetricSpace P₂] [inst_2 : PseudoEMetricSpace P₃]
  [inst_3 : PseudoEMetricSpace P₄] {F₁ : Type u_7} {F₂ : Type u_8} [inst_4 : FunLike F₁ P₁ P₃]
  [inst_5 : DilationClass F₁ P₁ P₃] [inst_6 : FunLike F₂ P₂ P₄] [inst_7 : DilationClass F₂ P₂ P₄] {f₁ : F₁} {f₂ : F₂},
  Congruent v₁ v₂ → Dilation.ratio f₁ = Dilation.ratio f₂ → Congruent (⇑f₁ ∘ v₁) (⇑f₂ ∘ v₂)

Two sets of vertices remain congruent under a dilation if the dilations have equal ratios.

Defined in

Mathlib.Topology.MetricSpace.Congruence

Cited by

0 results in Mathlib

Foundations

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

Assumes

PseudoEMetricSpacePseudoEMetricSpacePseudoEMetricSpacePseudoEMetricSpaceFunLikeDilationClassFunLikeDilationClass