isTransitiveRel_ball — Mathlib

English

For an ultrametric, the relation { (x,y) | d(x,y) < ε } is transitive.

Русский

Ультраметрическое расстояние обеспечивает транзитивность отношения { (x,y) | d(x,y) < ε }.

LaTeX

$$$ IsTransitiveRel \{(x,y) \mid d(x,y) < ε\}. $$$

Lean4

theorem isTransitiveRel_ball [Add R] [Zero R] [LinearOrder R] (d : PseudoMetric X R) [d.IsUltra] {ε : R} :
    IsTransitiveRel {xy | d xy.1 xy.2 < ε} := fun _ _ _ hxy hyz ↦ le_sup.trans_lt (max_lt hxy hyz)

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