exact — Mathlib

English

Equality of two words in FreeGroup corresponds to the join in the reduction relation: mk L1 = mk L2 iff Join Red L1 L2.

Русский

Равенство слов mk L1 и mk L2 в свободной группе эквивалентно достижимости через объединение Red: mk L1 = mk L2 тогда и только тогда, когда Join Red L1 L2.

LaTeX

$$$mk\\ L_1 = mk\\ L_2 \\iff Join\\ FreeGroup.Red\\ L_1\\ L_2$$$

Lean4

@[to_additive]
theorem exact : mk L₁ = mk L₂ ↔ Join Red L₁ L₂ :=
  calc
    mk L₁ = mk L₂ ↔ EqvGen Red.Step L₁ L₂ := Iff.intro Quot.eqvGen_exact Quot.eqvGen_sound
    _ ↔ Join Red L₁ L₂ := eqvGen_step_iff_join_red

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