cutExpand_double — Mathlib

English

If r(a1,a) and r(a2,a), then CutExpand r {a1, a2} {a}.

Русский

Если r(a1,a) и r(a2,a), то CutExpand r {a1, a2} {a}.

LaTeX

$$$\\forall a,a_1,a_2:\\; r(a_1,a) \\land r(a_2,a) \\Rightarrow \\mathrm{CutExpand}(r)({a_1,a_2},{a})$$$

Lean4

theorem cutExpand_double {a a₁ a₂} (h₁ : r a₁ a) (h₂ : r a₂ a) : CutExpand r { a₁, a₂ } { a } :=
  cutExpand_singleton <|
    by
    simp only [insert_eq_cons, mem_cons, mem_singleton, forall_eq_or_imp, forall_eq]
    tauto

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