btw_coe_iff — Mathlib

English

The between relation on the quotient is characterized by the inequality between the corresponding IcoMod and IocMod values after shifting.

Русский

Отношение между на фактор-группе характеризуется неравенством между соответствующими значениями IcoMod и IocMod после сдвига.

LaTeX

$$$$ \\text{btw\_coe\_iff}(x_1,x_2,x_3) \\Longleftrightarrow \\operatorname{toIcoMod}(hp'.out, x_1, x_2) \\le \\operatorname{toIocMod}(hp'.out, x_1, x_3) $$$$

Lean4

theorem btw_coe_iff {x₁ x₂ x₃ : α} :
    Btw.btw (x₁ : α ⧸ AddSubgroup.zmultiples p) x₂ x₃ ↔ toIcoMod hp'.out x₁ x₂ ≤ toIocMod hp'.out x₁ x₃ := by
  rw [btw_coe_iff', toIocMod_sub_eq_sub, toIcoMod_sub_eq_sub, zero_add, sub_le_sub_iff_right]

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