toDual_compl

Mathlib.Order.Heyting.Basic

URI: https://scilib.ai/kg/mathlib#toDual_compl

English

The dual of a complement equals the negation of the dual: toDual(aᶜ) = ¬ toDual(a).

Русский

Двойственность комплемента равна отрицанию двойственности: toDual(aᶜ) = ¬ toDual(a).

LaTeX

$$$\mathrm{toDual}(a^{\complement}) = \neg\mathrm{toDual}(a)$$$

Lean4

@[simp]
theorem toDual_compl (a : α) : toDual aᶜ = ￢toDual a :=
  rfl

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

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

Разделы

Аффилиация

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