pairwise

Mathlib.Data.Set.Pairwise.Basic

URI: https://scilib.ai/kg/mathlib#Set.Subsingleton.pairwise

English

If s is a subsingleton, then s is pairwise with respect to any relation r.

Русский

Если s — подсущность, то она попарно относится к любому отношению r.

LaTeX

$$$\forall {r : \alpha \to \alpha \to \mathrm{Prop}} (s : Set \alpha), s.Subsingleton \to s.Pairwise r$$$

Lean4

protected theorem pairwise (h : s.Subsingleton) (r : α → α → Prop) : s.Pairwise r := fun _x hx _y hy hne =>
  (hne (h hx hy)).elim

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

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

Разделы

Аффилиация

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