instIsEquiv

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#Order.Preimage.instIsEquiv

English

If r is an equivalence relation on α, then the preimage order on β is an equivalence relation.

Русский

Если $r$ — эквивалентность на $\alpha$, то $f^{-1'o r}$ — эквивалентность на β.

LaTeX

$$IsEquiv(β, (f⁻¹'o r))$$

Lean4

instance instIsEquiv [IsEquiv α r] {f : β → α} : IsEquiv β (f ⁻¹'o r) where

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

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

Разделы

Аффилиация

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