inv_mono

Mathlib.Data.Rel

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

English

If R1 ⊆ R2, then their inverses satisfy R1^{-1} ⊆ R2^{-1}.

Русский

Если R1 ⊆ R2, то их обратные отношения удовлетворяют R1^{-1} ⊆ R2^{-1}.

LaTeX

$$R_1 \subseteq R_2 \implies R_1^{-1} \subseteq R_2^{-1}$$

Lean4

@[gcongr]
theorem inv_mono (h : R₁ ⊆ R₂) : R₁.inv ⊆ R₂.inv := fun (_a, _b) hab ↦ h hab

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

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

Разделы

Аффилиация

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