mem_iff

Mathlib.Data.List.Rotate

URI: https://scilib.ai/kg/mathlib#List.IsRotated.mem_iff

English

Membership of an element is preserved under rotation: for all a, a ∈ l iff a ∈ l' whenever l ~r l'.

Русский

Членство элемента сохраняется при вращении: для любого a, a ∈ l эквивалентно a ∈ l' при условии l ~r l'.

LaTeX

$$$ l \sim_{\mathrm{rot}} l' \Rightarrow \forall a, a \in l \iff a \in l' $$$

Lean4

theorem mem_iff (h : l ~r l') {a : α} : a ∈ l ↔ a ∈ l' :=
  h.perm.mem_iff

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

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

Разделы

Аффилиация

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