cutExpand_double_left — Mathlib

English

Let r be a relation on α. If a1 is related to a and a2 is related to a, then the multiset {a1, a2, b} is related to {a, b} via CutExpand r.

Русский

Пусть r — отношение на α. Если a1 связано с a и a2 связано с a, то мультимножество {a1, a2, b} связано с {a, b} через CutExpand r.

LaTeX

$$$ r(a_1, a) \land r(a_2, a) \Rightarrow CutExpand(r, \{a_1, a_2, b\}, \{a, b\}) $$$

Lean4

theorem cutExpand_double_left {a a₁ a₂ b} (h₁ : r a₁ a) (h₂ : r a₂ a) : CutExpand r { a₁, a₂, b } { a, b } :=
  (cutExpand_add_right { b }).2 (cutExpand_double h₁ h₂)

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