pairwise_coe_iff — Mathlib

English

For any r and l, Multiset.Pairwise r (ofList l) holds iff there exists l' with l ~ l' and l'.Pairwise r.

Русский

Для любого r и списка l, Multiset.Pairwise r (ofList l) выполняется тогда и только тогда, когда существует l' such that l ~ l' и l'.Pairwise r.

LaTeX

$$$\\forall r\\, l,\\ Multiset.Pairwise\\ r\\ (\\operatorname{ofList}l)\\;\\Leftrightarrow\\;\\exists l'\\;:\\text{List}(\\alpha),\\ l\\sim l'\\wedge l'.Pairwise r$$$

Lean4

theorem pairwise_coe_iff {r : α → α → Prop} {l : List α} :
    Multiset.Pairwise r l ↔ ∃ l' : List α, l ~ l' ∧ l'.Pairwise r :=
  exists_congr <| by simp

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