isCyclicallyReduced_cons_append_iff

English

For any a,b ∈ α×Bool and any L, IsCyclicallyReduced (b :: L ++ [a]) holds if and only if IsReduced (b :: L ++ [a]) and a.fst = b.fst → a.snd = b.snd.

Русский

Для любых a,b ∈ α×Bool и любого L верно: IsCyclicallyReduced (b :: L ++ [a]) тогда и только тогда, когда IsReduced (b :: L ++ [a]) и a.fst = b.fst → a.snd = b.snd.

LaTeX

$$$$ \\mathrm{IsCyclicallyReduced}(b :: L ++ [a]) \\iff \\mathrm{IsReduced}(b :: L ++ [a]) \\land (a.fst = b.fst \\rightarrow a.snd = b.snd). $$$$

Lean4

@[to_additive]
theorem isCyclicallyReduced_cons_append_iff {a b : α × Bool} :
    IsCyclicallyReduced (b :: L ++ [a]) ↔ IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2) :=
  by
  rw [isCyclicallyReduced_iff, List.getLast?_concat]
  simp

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