lf_iff_sub_zero_lf — Mathlib

English

The left-fuzzy relation between x and y is equivalent to the left-fuzzy relation between 0 and y − x.

Русский

Леволюбивое отношение между x и y эквивалентно леволюбивому отношению между 0 и y − x.

LaTeX

$$$ x \\;\\text{LF} \\; y \\iff 0 \\;\\text{LF} \\; (y - x) $$$

Lean4

theorem lf_iff_sub_zero_lf {x y : PGame} : x ⧏ y ↔ 0 ⧏ y - x :=
  ⟨fun h => (zero_le_add_neg_cancel x).trans_lf (add_lf_add_right h _), fun h =>
    calc
      x ≤ 0 + x := (PGame.zero_add x).symm.le
      _ ⧏ y - x + x := (add_lf_add_right h _)
      _ ≤ y + (-x + x) := (PGame.add_assoc _ _ _).le
      _ ≤ y + 0 := (add_le_add_left (neg_add_cancel_le_zero x) _)
      _ ≤ y := (PGame.add_zero y).le⟩

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