mem_sym2_iff

Mathlib.Data.List.Sym

URI: https://scilib.ai/kg/mathlib#List.mem_sym2_iff

English

For any xs and z ∈ xs.sym2, z ∈ xs sym2 iff every y in z belongs to xs.

Русский

Для любого xs и z ∈ xs.sym2, z ∈ xs.sym2 тогда, когда все элементы z принадлежат xs.

LaTeX

$$$$ z \\in xs.sym2 \\iff ∀ y \\in z, y \\in xs $$$$

Lean4

theorem mem_sym2_iff {xs : List α} {z : Sym2 α} : z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs :=
  by
  refine z.ind (fun a b => ?_)
  simp [mk_mem_sym2_iff]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru