himp_compl

Mathlib.Order.Heyting.Basic

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

English

For all a, a ⇨ aᶜ = aᶜ.

Русский

Для любого a: a ⇨ aᶜ = aᶜ.

LaTeX

$$$ a \\Rightarrow a^{\\complement} = a^{\\complement} $$$

Lean4

@[simp]
theorem himp_compl (a : α) : a ⇨ aᶜ = aᶜ := by
  rw [← himp_bot, himp_himp, inf_idem]
    -- `p → ¬ q ↔ q → ¬ p`

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

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

Разделы

Аффилиация

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