fromRel_toRel

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.fromRel_toRel

English

For any set s, applying toRel_symmetric to s and then fromRel returns the original set.

Русский

Для любого множества s применение fromRel к toRel_symmetric(s) восстанавливает исходное множество.

LaTeX

$$$$ \mathrm{fromRel}(\mathrm{toRel\_symmetric}(s)) = s. $$$$

Lean4

theorem fromRel_toRel (s : Set (Sym2 α)) : fromRel (toRel_symmetric s) = s :=
  Set.ext fun z => Sym2.ind (fun _ _ => Iff.rfl) z

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

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

Разделы

Аффилиация

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