subtype — Mathlib

English

If X is ultrametric and p is a predicate on X, then the subtype {x ∈ X : p(x)} inherits an ultrametric distance from X.

Русский

Если X ультраметрическое пространство и p — предикат над X, то подпространство {x ∈ X : p(x)} наследует ультраметрическое расстояние от X.

LaTeX

$$∀ a,b,c ∈ Subtype(p),\ d(a,c) ≤ max(d(a,b), d(b,c)).$$

Lean4

instance subtype (p : X → Prop) : IsUltrametricDist (Subtype p) :=
  ⟨fun _ _ _ ↦ by simpa [Subtype.dist_eq] using dist_triangle_max _ _ _⟩

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