isTrans_preimage

Mathlib.Data.Rel

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

English

If R is transitive on α, then its preimage under a map f: β → α, i.e. (Prod.map f f)^{-1}' R, is transitive.

Русский

Если R на α транзитивно, то предобраз под отображением f: β → α транзитивен.

LaTeX

$$$\text{SetRel.IsTrans} (Prod.map f f \;^{-1}'\; R)$$$

Lean4

instance isTrans_preimage {f : β → α} [R.IsTrans] : SetRel.IsTrans (Prod.map f f ⁻¹' R) where trans _ _ _ := R.trans

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

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

Разделы

Аффилиация

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