instIsRelIffOp

Mathlib.Algebra.Homology.Embedding.Basic

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.instIsRelIffOp

English

If e is an embedding with IsRelIff, then its opposite embedding e.op also has IsRelIff.

Русский

Если e — вложение с IsRelIff, то и противоположное вложение e.op тоже имеет IsRelIff.

LaTeX

$$$ [e.IsRelIff] \\Rightarrow [e.op.IsRelIff] $$$

Lean4

instance [e.IsRelIff] : e.op.IsRelIff where rel' i₁ i₂ h := (e.rel_iff i₂ i₁).1 h

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

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

Разделы

Аффилиация

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