isTransitiveRel_closedBall — Mathlib

English

Similarly, the relation { (x,y) | d(x,y) ≤ ε } is transitive under ultrametric-like assumptions.

Русский

Аналогично, отношение с ≤ ε транзитивно.

LaTeX

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

Lean4

theorem isTransitiveRel_closedBall [Add R] [Zero R] [SemilatticeSup R] (d : PseudoMetric X R) [d.IsUltra] {ε : R} :
    IsTransitiveRel {xy | d xy.1 xy.2 ≤ ε} := fun _ _ _ hxy hyz ↦ le_sup.trans (sup_le hxy hyz)

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