symm

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Codisjoint.symm

English

If Codisjoint a b then Codisjoint b a.

Русский

Если a ⊥ b, то b ⊥ a.

LaTeX

$$$\operatorname{Codisjoint}(a,b) \to \operatorname{Codisjoint}(b,a)$$$

Lean4

@[symm]
theorem symm ⦃a b : α⦄ : Codisjoint a b → Codisjoint b a :=
  codisjoint_comm.1

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

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

Разделы

Аффилиация

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