instPreorderWithPreorder — Mathlib

English

Let R be a commutative ring equipped with a valuative relation. Then the relation ≤ᵥ on R defines a preorder on WithPreorder R by setting x ≤ y if x ≤ᵥ y.

Русский

Пусть R — коммутативное кольцо, снабжённое валуативным отношением. Тогда отношение ≤ᵥ на R задаёт предпорядок на WithPreorder R, если x ≤ y тогда x ≤ᵥ y.

LaTeX

$$$\\text{Preorder}(\\mathrm{WithPreorder}(R)) \\\\text{with } \\le := \\le_{\\mathrm{v}}.$$$

Lean4

/-- The preorder on `WithPreorder R` arising from the valuative relation on `R`. -/
instance : Preorder (WithPreorder R) where
  le (x y : R) := x ≤ᵥ y
  le_refl _ := rel_refl _
  le_trans _ _ _ := rel_trans

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