instExistsAddOfLE — Mathlib

English

WithZero α carries a preorder structure extending α's, defined by lt_iff_le_not_ge and related lemmas.

Русский

WithZero α наследует предикатный порядок от α, определяемый через lt_iff_le_not_ge и сопутствующие леммы.

LaTeX

$$$ x < y \iff x < y \text{ defined by extended preorder on } \mathrm{WithZero} \alpha $$$

Lean4

instance instExistsAddOfLE [Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithZero α) :=
  ⟨fun {a b} => by
    induction a
    · exact fun _ => ⟨b, (zero_add b).symm⟩
    induction b
    · exact fun h => (not_coe_le_zero h).elim
    intro h
    obtain ⟨c, rfl⟩ := exists_add_of_le (WithZero.coe_le_coe.1 h)
    exact ⟨c, rfl⟩⟩

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