set_pairwise

Mathlib.Data.List.Pairwise

URI: https://scilib.ai/kg/mathlib#List.Pairwise.set_pairwise

English

If l is Pairwise R, and R is symmetric, then the set {x | x ∈ l} is Pairwise R.

Русский

Если для множества элементов l выполняется Pairwise R и R симметрично, то множество {x | x ∈ l} является Pairwise R.

LaTeX

$$$\\{x \\mid x \\in l\\}.\\text{Pairwise}(R).$$$

Lean4

theorem set_pairwise (hl : Pairwise R l) (hr : Symmetric R) : {x | x ∈ l}.Pairwise R :=
  hl.forall hr

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

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

Разделы

Аффилиация

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