red_iff_irreducible — Mathlib

English

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

Русский

Эквивгенция редукций между L1 и L2 эквивалентна соединению Red L1 L2.

LaTeX

$$$EqvGen\,Red.Step\,L_1\,L_2 \;\leftrightarrow\; Join\,Red\,L_1\,L_2$$$

Lean4

@[to_additive]
theorem red_iff_irreducible {x1 b1 x2 b2} (h : (x1, b1) ≠ (x2, b2)) :
    Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)] :=
  by
  apply reflTransGen_iff_eq
  generalize eq : [(x1, not b1), (x2, b2)] = L'
  intro L h'
  cases h'
  simp only [List.cons_eq_append_iff, List.cons.injEq, Prod.mk.injEq, and_false, List.nil_eq_append_iff, exists_const,
    or_self, or_false, List.cons_ne_nil] at eq
  rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩
  simp at h

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