dist_zero_of_empty — Mathlib

English

If α is empty, then for any f,g : α →ᵇ β we have dist f g = 0, since f = g by extensionality on the empty domain.

Русский

Если α пусто, то для любых f,g : α →ᵇ β выполняется dist f g = 0, так как f = g из-за пустого домена.

LaTeX

$$[IsEmpty α] ⇒ dist f g = 0$$

Lean4

/-- On an empty space, bounded continuous functions are at distance 0. -/
theorem dist_zero_of_empty [IsEmpty α] : dist f g = 0 := by rw [(ext isEmptyElim : f = g), dist_self]

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