snd_compl

Mathlib.Order.Heyting.Basic

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

English

In α × β with HasCompl, the second projection of aᶜ equals the complement of the second projection: aᶜ₂ = a₂ᶜ.

Русский

В α × β с HasCompl, вторая проекция aᶜ равна комплементу второй проекции: aᶜ₂ = a₂ᶜ.

LaTeX

$$$ a^\complement_2 = a_2^\complement $$$

Lean4

@[simp]
theorem snd_compl [HasCompl α] [HasCompl β] (a : α × β) : aᶜ.2 = a.2ᶜ :=
  rfl

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

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

Разделы

Аффилиация

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