compl

Mathlib.Order.Antichain

URI: https://scilib.ai/kg/mathlib#Symmetric.compl

English

If a relation r on a set is symmetric, then its complement r^c is also symmetric.

Русский

Если отношение r на множестве симметрично, то его дополнение r^c также симметрично.

LaTeX

$$$ \forall \alpha, \beta, r: \alpha \to \alpha \to Prop, (\text{Symmetric } r) \to \text{Symmetric } r^c $$$

Lean4

protected theorem compl (h : Symmetric r) : Symmetric rᶜ := fun _ _ hr hr' => hr <| h hr'

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

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

Разделы

Аффилиация

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