instPartialOrder — Mathlib

English

The collection of pseudo metrics is equipped with a pointwise order: d ≤ d' iff d(x,y) ≤ d'(x,y) for all x,y.

Русский

Набор псевдометрик упорядочен по точечному порядку: d ≤ d' тогда и только тогда, когда d(x,y) ≤ d'(x,y) для всех x,y.

LaTeX

$$$d \le d' \iff \forall x,y,\; d(x,y) \le d'(x,y).$$$

Lean4

instance [Zero R] [Add R] [PartialOrder R] : PartialOrder (PseudoMetric X R) :=
  .lift _ DFunLike.coe_injective

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