pairwise_pair_of_symmetric

Mathlib.Data.Set.Pairwise.Basic

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

English

If r is symmetric, then {a,b} is pairwise w.r.t r iff a ≠ b implies r a b.

Русский

Если r симметрично, то {a,b} попарно по r тогда, когда a ≠ b ⇒ r a b.

LaTeX

$$$(hr) \Rightarrow (Set.Pairwise {a,b} r \leftrightarrow a \neq b \to r a b)$$$

Lean4

theorem pairwise_pair_of_symmetric (hr : Symmetric r) : Set.Pairwise { a, b } r ↔ a ≠ b → r a b := by
  simp [pairwise_insert_of_symmetric hr]

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

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

Разделы

Аффилиация

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