set_pairwise

Mathlib.Logic.Pairwise

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

English

If h is Pairwise on r, then h holds for any set s: s.Pairwise r.

Русский

Если h попарно по r, то он держится на любом множестве s: s.Pairwise r.

LaTeX

$$$\\operatorname{Pairwise}(r) \\Rightarrow \\operatorname{Set.Pairwise}(s,r)$$$

Lean4

theorem set_pairwise (h : Pairwise r) (s : Set α) : s.Pairwise r := fun _ _ _ _ w => h w

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

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

Разделы

Аффилиация

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