metricSpace — Mathlib

English

For any predicate p, the subtype {x ∈ α | p x} carries a natural metric space structure induced from α via the inclusion map.

Русский

Подмножество вида {x ∈ α | p x} имеет естественную метрическую структуру, полученную из α через включение.

LaTeX

$$$ \text{Subtype.metricSpace } (p) : \text{MetricSpace} (Subtype p)$$$

Lean4

instance metricSpace {α : Type*} {p : α → Prop} [MetricSpace α] : MetricSpace (Subtype p) :=
  .induced Subtype.val Subtype.coe_injective ‹_›

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