of_reduce_eq — Mathlib

English

If reduce L = L, then L is reduced.

Русский

Если редукция L равна L, то L редуцировано.

LaTeX

$$$\mathrm{reduce} L = L \Rightarrow \mathrm{IsReduced} L$$$

Lean4

@[to_additive]
theorem of_reduce_eq (h : reduce L = L) : IsReduced L :=
  by
  rw [IsReduced, List.isChain_iff_forall_rel_of_append_cons_cons]
  rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ l₁ l₂ hl rfl
  rw [eq_comm, ← Bool.ne_not]
  rintro rfl
  exact reduce.not (h.trans hl)

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