eqvGen_step_iff_join_red — Mathlib

English

EqvGen Red.Step between L1 and L2 is equivalent to Join Red L1 L2.

Русский

EqvGen Red.Step между L1 и L2 эквивалентна Join Red L1 L2.

LaTeX

$$$EqvGen\;Red.Step\;L_1\;L_2 \iff Join\;Red\;L_1\;L_2$$$

Lean4

@[to_additive]
theorem eqvGen_step_iff_join_red : EqvGen Red.Step L₁ L₂ ↔ Join Red L₁ L₂ :=
  Iff.intro
    (fun h =>
      have : EqvGen (Join Red) L₁ L₂ := h.mono fun _ _ => join_red_of_step
      equivalence_join_red.eqvGen_iff.1 this)
    (join_of_equivalence (Relation.EqvGen.is_equivalence _) fun _ _ =>
      reflTransGen_of_equivalence (Relation.EqvGen.is_equivalence _) EqvGen.rel)

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