mem_of_perm — Mathlib

English

If s1.entries is a permutation of s2.entries, then for every a, a ∈ s1 iff a ∈ s2.

Русский

Если entries s1 является перестановкой entries s2, то для любого a выполнено a ∈ s1 ⇔ a ∈ s2.

LaTeX

$$s_1.entries \sim s_2.entries \Rightarrow (a \in s_1 \iff a \in s_2)$$

Lean4

theorem mem_of_perm {a : α} {s₁ s₂ : AList β} (p : s₁.entries ~ s₂.entries) : a ∈ s₁ ↔ a ∈ s₂ :=
  (p.map Sigma.fst).mem_iff

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