cutExpand_pair_right — Mathlib

English

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

Русский

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

LaTeX

$$$ r(b', b) \Rightarrow CutExpand(r, \{a, b'\}, \{a, b\}) $$$

Lean4

theorem cutExpand_pair_right {a b' b} (hr : r b' b) : CutExpand r { a, b' } { a, b } :=
  (cutExpand_add_left { a }).2 (cutExpand_singleton_singleton hr)

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