instOrderedAddOfAddRightMonoOfAddRightReflectLE

English

If M is additive, has a preorder, and both AddRightMono and AddRightReflectLE, then there is an OrderedAdd structure on M with add_le_left_iff given by these properties.

Русский

Если M — множество с операцией сложения, задано отношением порядка и выполняются AddRightMono и AddRightReflectLE, то на M существует структура упорядоченного сложения, задаваемая через add_le_left_iff.

LaTeX

$$OrderedAdd on M exists with add_le_left_iff := fun c => ⟨AddRightMono.elim c, AddRightReflectLE.elim c⟩$$

Lean4

instance [Add M] [Preorder M] [i₁ : AddRightMono M] [i₂ : AddRightReflectLE M] : Lean.Grind.OrderedAdd M where
  add_le_left_iff := fun c => ⟨i₁.elim c, i₂.elim c⟩

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