r — Mathlib · SciLib

English

The relation r on M × S is defined by (m1,s1) ~ (m2,s2) if there exists u ∈ S with u·s2·m1 = u·s1·m2.

Русский

Отношение r на паре (m, s) определяется как (m1, s1) ~ (m2, s2) если существует u ∈ S такое, что u·s2·m1 = u·s1·m2.

LaTeX

$$$r_S^M((m_1,s_1),(m_2,s_2)) \\iff \\exists u \\in S,\\ u\\,; b.2\\; a.1 = u\\,; a.2\\; b.1$$$

Lean4

/-- The equivalence relation on `M × S` where `(m1, s1) ≈ (m2, s2)` if and only if
for some (u : S), u * (s2 • m1 - s1 • m2) = 0 -/
def r (a b : M × S) : Prop :=
  ∃ u : S, u • b.2 • a.1 = u • a.2 • b.1

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