add_eq_max_of_ne — Mathlib

English

If f x ≠ f y, then f(x + y) = max(f(x), f(y)).

Русский

Если f(x) ≠ f(y), то f(x + y) = max{f(x), f(y)}.

LaTeX

$$$f(x+y) = \\max\\{f(x), f(y)\\}$ whenever $f(x) \\neq f(y)$$$

Lean4

/-- 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)`. -/
theorem add_eq_max_of_ne {F α : Type*} [AddGroup α] [FunLike F α R] [AddGroupSeminormClass F α R] {f : F}
    (hna : IsNonarchimedean f) {x y : α} (hne : f x ≠ f y) : f (x + y) = max (f x) (f y) :=
  by
  rcases hne.lt_or_gt with h_lt | h_lt
  · rw [add_eq_right_of_lt hna h_lt]
    exact (max_eq_right_of_lt h_lt).symm
  · rw [add_eq_left_of_lt hna h_lt]
    exact (max_eq_left_of_lt h_lt).symm

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