rel_cons_right — Mathlib

English

Rel r as (b ::ₘ bs) holds exactly when there exists a and as' with r a b, Rel r as' bs, and as = a ::ₘ as'.

Русский

Rel r as (b ::ₘ bs) выполняется тогда, когда существует a и as' такие, что r a b, Rel r as' bs и as = a ::ₘ as'.

LaTeX

$$$Rel\ r\ as (Multiset.cons b\ bs) \iff \exists a\ exists as' , r\ a\ b \land Rel\ r\ as'\ bs \land as = a ::ₘ as'$$$

Lean4

theorem rel_cons_right {as b bs} : Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as' :=
  by
  rw [← rel_flip, rel_cons_left]
  refine exists₂_congr fun a as' => ?_
  rw [rel_flip, flip]

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