add_le — Mathlib

English

If there exists an order-preserving injective map f:S→R into a strict ordered ring R that preserves 0,1 and the ring operations, then S is a strict ordered ring.

Русский

Если существует инъективное отображение f:S→R, сохраняющее порядок и кольцевые операции, в строго упорядоченное кольцо R, то S также образует строго упорядоченное кольцо.

LaTeX

$$$\exists f:S\to R\; (\text{injective})\land f(0)=0\land f(1)=1\land f(x+y)=f(x)+f(y)\land f(xy)=f(x)f(y)\land (x\le y \iff f(x)\le f(y))\land (x

Lean4

/-- A nonnegative nonarchimedean function satisfies the triangle inequality. -/
theorem add_le [IsStrictOrderedRing R] {α : Type*} [Add α] {f : α → R} (hf : ∀ x : α, 0 ≤ f x)
    (hna : IsNonarchimedean f) {a b : α} : f (a + b) ≤ f a + f b :=
  by
  apply le_trans (hna _ _)
  rw [max_le_iff, le_add_iff_nonneg_right, le_add_iff_nonneg_left]
  exact ⟨hf _, hf _⟩

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