add_eq_left_of_lt — Mathlib

English

If f y < f x, then f(x + y) = f(x).

Русский

Если f(y) < f(x), то f(x + y) = f(x).

LaTeX

$$$\\forall x,y,\\; f(y) < f(x) \\Rightarrow f(x+y) = f(x)$$$

Lean4

theorem add_eq_left_of_lt {F α : Type*} [AddGroup α] [FunLike F α R] [AddGroupSeminormClass F α R] {f : F}
    (hna : IsNonarchimedean f) {x y : α} (h_lt : f y < f x) : f (x + y) = f x :=
  by
  by_contra! h
  have h1 : f (x + y) ≤ f x := (hna x y).trans_eq (max_eq_left_of_lt h_lt)
  apply lt_irrefl (f x)
  calc
    f x = f (x + y + -y) := by simp
    _ ≤ max (f (x + y)) (f (-y)) := (hna (x + y) (-y))
    _ < max (f x) (f x) := by
      rw [max_self, map_neg_eq_map]
      apply max_lt (lt_of_le_of_ne h1 h) h_lt
    _ = f x := max_self (f x)

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