get_le_get — Mathlib

English

The comparison of numbers via get is consistent with the overall order: x.get(hx) ≤ y.get(hy) is equivalent to x ≤ y.

Русский

Сравнение через get согласуется с общим порядком: x.get(hx) ≤ y.get(hy) эквивалентно x ≤ y.

LaTeX

$$$ x.get(h_x) \le y.get(h_y) \iff x \le y $$$

Lean4

@[simp]
theorem get_le_get {x y : PartENat} {hx : x.Dom} {hy : y.Dom} : x.get hx ≤ y.get hy ↔ x ≤ y := by
  conv =>
    lhs
    rw [← coe_le_coe, natCast_get, natCast_get]

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