isReduced_cons_cons — Mathlib

English

For any a,b and L, IsReduced(a :: b :: L) holds iff (a.fst = b.fst → a.snd = b.snd) and IsReduced(b :: L).

Русский

Для любых a,b и L, IsReduced(a :: b :: L) равносильно (a.fst = b.fst → a.snd = b.snd) и IsReduced(b :: L).

LaTeX

$$$\operatorname{IsReduced}(a \,::\, b \,::\, L) \iff \big(a_1 = b_1 \to a_2 = b_2\big) \land \operatorname{IsReduced}(b \,::\, L).$$$

Lean4

@[to_additive (attr := simp)]
theorem isReduced_cons_cons {a b : (α × Bool)} :
    IsReduced (a :: b :: L) ↔ (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: L) :=
  isChain_cons_cons

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