unzero_le_unzero — Mathlib

English

For nonzero elements a,b ∈ WithZero α (ha,hb), their unzero images satisfy a ≤ b in α iff a ≤ b in WithZero α.

Русский

Для ненулевых элементов a,b ∈ WithZero α (ha,hb) их изображения без нуля удовлетворяют a ≤ b в α тогда и только тогда, когда a ≤ b в WithZero α.

LaTeX

$$$ \operatorname{unzero}(ha) \le \operatorname{unzero}(hb) \iff a \le b $$$

Lean4

@[simp]
theorem unzero_le_unzero {a b : WithZero α} (ha hb) : unzero (x := a) ha ≤ unzero (x := b) hb ↔ a ≤ b := by
  -- TODO: Fix `lift` so that it doesn't try to clear the hypotheses I give it when it is
    -- impossible to do so. See https://github.com/leanprover-community/mathlib4/issues/19160

  lift a to α using id ha
  lift b to α using id hb
  simp

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