instHNot

Mathlib.Order.Heyting.Basic

URI: https://scilib.ai/kg/mathlib#Prod.instHNot

English

Negation in a product is defined componentwise: ￢(a1,a2) = (￢a1, ￢a2).

Русский

Отрицание на произведении определяется по компонентам: ¬(a1,a2) = (¬a1, ¬a2).

LaTeX

$$¬(a_1, a_2) = (¬a_1, ¬a_2)$$

Lean4

instance instHNot [HNot α] [HNot β] : HNot (α × β) :=
  ⟨fun a => (￢a.1, ￢a.2)⟩

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

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

Разделы

Аффилиация

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