pairwise_of_forall

Mathlib.Logic.Pairwise

URI: https://scilib.ai/kg/mathlib#Set.pairwise_of_forall

English

If r holds for all pairs, then s is pairwise with respect to r.

Русский

Если r держится для всех пар, то s попарно относительно r.

LaTeX

$$$\\forall a,b,\\ r(a,b) \\Rightarrow s.\\Pairwise r$$$

Lean4

theorem pairwise_of_forall (s : Set α) (r : α → α → Prop) (h : ∀ a b, r a b) : s.Pairwise r := fun a _ b _ _ => h a b

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

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

Разделы

Аффилиация

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