val_eq — Mathlib

English

If v1 is equivalent to v2, then for all r,s in R, v1(r) = v1(s) if and only if v2(r) = v2(s).

Русский

Если v1 эквивалентна v2, то для всех r,s в R верно: v1(r) = v1(s) тогда и только тогда, когда v2(r) = v2(s).

LaTeX

$$$ (v_1 \IsEquiv v_2) \rightarrow \forall r,s:\, R, (v_1(r) = v_1(s)) \iff (v_2(r) = v_2(s)) $$$

Lean4

theorem val_eq (h : v₁.IsEquiv v₂) {r s : R} : v₁ r = v₁ s ↔ v₂ r = v₂ s := by
  simpa only [le_antisymm_iff] using and_congr (h r s) (h s r)

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