isSupportedOutside₂_iff

Mathlib.Algebra.Homology.Embedding.AreComplementary

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.AreComplementary.isSupportedOutside₂_iff

English

Symmetric counterpart to the previous: K.IsSupportedOutside e2 iff K.IsSupported e1.

Русский

Аналогично: K.IsSupportedOutside e2 эквивално K.IsSupported e1.

LaTeX

$$$K.IsSupportedOutside\ e_2 \iff K.IsSupported\ e_1.$$$

Lean4

theorem isSupportedOutside₂_iff : K.IsSupportedOutside e₂ ↔ K.IsSupported e₁ :=
  ac.symm.isSupportedOutside₁_iff K

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

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

Разделы

Аффилиация

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