isSymm_preimage

Mathlib.Data.Rel

URI: https://scilib.ai/kg/mathlib#SetRel.isSymm_preimage

English

If R is symmetric, then the preimage relation Prod.map f f ⁻¹' R is symmetric.

Русский

Если R симметрично, то прообразная по f связь на β через R симметрична.

LaTeX

$$If [R.IsSymm], then SetRel.IsSymm (Set.preimage (Prod.map f f) R)$$

Lean4

instance isSymm_preimage {f : β → α} [R.IsSymm] : SetRel.IsSymm (Prod.map f f ⁻¹' R) where symm _ _ := R.symm

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

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

Разделы

Аффилиация

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