le_of_le_le — Mathlib

English

If x ≤ z and y ≤ w for integers, then ⟨x,y⟩ ≤ ⟨z,w⟩ in Z√d.

Русский

Если x ≤ z и y ≤ w, то ⟨x,y⟩ ≤ ⟨z,w⟩ в Z√d.

LaTeX

$$x ≤ z ∧ y ≤ w ⇒ (⟨x,y⟩ ≤ ⟨z,w⟩)$$

Lean4

theorem le_of_le_le {x y z w : ℤ} (xz : x ≤ z) (yw : y ≤ w) : (⟨x, y⟩ : ℤ√d) ≤ ⟨z, w⟩ :=
  show Nonneg ⟨z - x, w - y⟩ from
    match z - x, w - y, Int.le.dest_sub xz, Int.le.dest_sub yw with
    | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => trivial

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