symm

Mathlib.Data.WSeq.Relation

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.LiftRel.symm

← MathLib Explorer

English

The lifted relation is symmetric if the base relation is symmetric.

Русский

Поднятое отношение симметрично, если базовое отношение симметрично.

LaTeX

$$$$ \mathrm{Symm}(R) \Rightarrow \mathrm{Symm}(\mathrm{LiftRel}\ R). $$$$

Lean4

theorem symm (R : α → α → Prop) (H : Symmetric R) : Symmetric (LiftRel R) :=
  fun s1 s2 (h : Function.swap (LiftRel R) s2 s1) => by rwa [LiftRel.swap, H.swap_eq] at h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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