mk_coe_of_dist_eq — Mathlib

English

Two definitions of Dilation coincide: mapping via Dilation.mkOfDistEq yields the same dilation as the original f.

Русский

Две конструкции дилатации совпадают: отображение через Dilation.mkOfDistEq дает такую же дилатацию, как исходная функция.

LaTeX

$$Dilation.mkOfDistEq f h = f$$

Lean4

@[simp]
theorem mk_coe_of_dist_eq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α →ᵈ β) (h) :
    Dilation.mkOfDistEq f h = f :=
  ext fun _ => rfl

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