Theorems · Theorem · order theory

IsNonarchimedean.add_eq_max_of_ne

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} [inst_2 : AddGroup α]
  [inst_3 : FunLike F α R] [AddGroupSeminormClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {x y : α}, f x ≠ f y → f (x + y) = max (f x) (f y)

If f is a nonarchimedean additive group seminorm on α and x y : α are such that f x ≠ f y, then f (x + y) = max (f x) (f y).

Defined in

Mathlib.Algebra.Order.Ring.IsNonarchimedean

Cited by

2 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

SemiringLinearOrderAddGroupFunLikeAddGroupSeminormClass