map_sub_le — Mathlib

English

Equivalence of valuations can be characterized by the pointwise equality of the induced preorder relations; i.e., equality of IsEquiv corresponds to equality of induced orderings on all pairs.

Русский

Эквивалентность оценок может быть охарактеризована равенством порожденных предобзоров; то есть равенство IsEquiv соответствует равенству соответствующих отношений порядка на всех парах.

LaTeX

$$$v_1.IsEquiv v_2 \\quad\\text{iff}\\quad \\forall r,s:\\, R,\\; (v_1(r) \\le v_1(s) \\iff v_2(r) \\le v_2(s))$$$

Lean4

theorem map_sub_le {x y g} (hx : v x ≤ g) (hy : v y ≤ g) : v (x - y) ≤ g :=
  by
  rw [sub_eq_add_neg]
  exact v.map_add_le hx <| (v.map_neg y).trans_le hy

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