Theorems · Theorem · order theory

IsNonarchimedean.add_le

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {α : Type u_2} [inst_3 : Add α]
  {f : α → R}, (∀ (x : α), 0 ≤ f x) → IsNonarchimedean f → ∀ {a b : α}, f (a + b) ≤ f a + f b

A nonnegative nonarchimedean function satisfies the triangle inequality.

Defined in

Mathlib.Algebra.Order.Ring.IsNonarchimedean

Cited by

1 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringLinearOrderIsStrictOrderedRingAdd