comp

Mathlib.Topology.MetricSpace.Dilation

URI: https://scilib.ai/kg/mathlib#Dilation.comp

Lean4

/-- The composition of dilations is a dilation -/
def comp (g : β →ᵈ γ) (f : α →ᵈ β) : α →ᵈ γ where
  toFun := g ∘ f
  edist_eq' :=
    ⟨ratio g * ratio f, mul_ne_zero (ratio_ne_zero g) (ratio_ne_zero f), fun x y => by
      simp_rw [Function.comp, edist_eq, ENNReal.coe_mul, mul_assoc]⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru