symm_iff

Mathlib.Data.Finmap

URI: https://scilib.ai/kg/mathlib#Finmap.Disjoint.symm_iff

English

Disjoint x y is equivalent to Disjoint y x: Disjoint x y ↔ Disjoint y x.

Русский

Дисjoint эквивалентно своей симметрии: Disjoint x y ↔ Disjoint y x.

LaTeX

$$$ \operatorname{Disjoint}(x,y) \iff \operatorname{Disjoint}(y,x) $$$

Lean4

theorem symm_iff (x y : Finmap β) : Disjoint x y ↔ Disjoint y x :=
  ⟨Disjoint.symm x y, Disjoint.symm y x⟩

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

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

Разделы

Аффилиация

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