pairwise_univ

Mathlib.Data.Set.Pairwise.Basic

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

English

The universal set is pairwise with respect to r iff r is pairwise on α.

Русский

Универсальное множество попарно по r тогда и только тогда, когда r попарно на α.

LaTeX

$$$(Set.univ.Pairwise r) \leftrightarrow (Set.Pairwise r)$$$

Lean4

theorem pairwise_univ : (univ : Set α).Pairwise r ↔ Pairwise r := by
  simp only [Set.Pairwise, Pairwise, mem_univ, forall_const]

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

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

Разделы

Аффилиация

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