dist_toBCF_eq_dist

Mathlib.Topology.ContinuousMap.ZeroAtInfty

URI: https://scilib.ai/kg/mathlib#ZeroAtInftyContinuousMap.dist_toBCF_eq_dist

English

Distances are preserved under the toBCF construction: dist f.toBCF g.toBCF = dist f g.

Русский

Расстояния сохраняются под преобразованием к toBCF: dist f.toBCF g.toBCF = dist f g.

LaTeX

$$dist\\_toBCF\\_eq\\_dist: ∀ f,g, dist(f.toBCF,g.toBCF)=dist(f,g)$$

Lean4

@[simp]
theorem dist_toBCF_eq_dist {f g : C₀(α, β)} : dist f.toBCF g.toBCF = dist f g :=
  rfl

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

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

Разделы

Аффилиация

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