Theorems · Definition · order theory

IsNonarchimedean

{R : Type u_3} → [LinearOrder R] → {α : Type u_4} → [Add α] → (α → R) → Prop

A function f : α → R is nonarchimedean if it satisfies the ultrametric inequality f (a + b) ≤ max (f a) (f b) for all a b : α.

Defined in

Mathlib.Algebra.Order.Ring.Basic

Cited by

77 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

LinearOrderAdd