btw_coe_iff' — Mathlib

English

In the quotient α / zmultiples p, the between relation Btw between x1, x2, x3 is equivalent to an inequality between toIcoMod and toIocMod of differences with x1.

Русский

В делеционном классе α / zmultiples p отношение between x1, x2, x3 эквивалентно неравенству между toIcoMod и toIocMod для разностей (x2 − x1) и (x3 − x1).

LaTeX

$$Btw.btw (x1 : α ⧸ AddSubgroup.zmultiples p) x2 x3 ↔ toIcoMod hp' 0 (x2 - x1) ≤ toIocMod hp' 0 (x3 - x1)$$

Lean4

theorem btw_coe_iff' {x₁ x₂ x₃ : α} :
    Btw.btw (x₁ : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ↔ toIcoMod hp'.out 0 (x₂ - x₁) ≤ toIocMod hp'.out 0 (x₃ - x₁) :=
  Iff.rfl

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