snd_hnot — Mathlib

English

Let α and β be Heyting algebras with a negation operation. For any a = (x, y) in α × β, the second coordinate of the negation of a equals the negation of the second coordinate: (¬a)₂ = ¬(a₂).

Русский

Пусть α и β — алгебры Хейтингa с операцией отрицания. Для любой пары a = (x, y) ∈ α × β верно, что второе координатное значение отрицания a равно отрицанию второго координатного значения a: (¬a)₂ = ¬(a₂).

LaTeX

$$$ (\neg a)_2 = \neg(a_2) $$$

Lean4

@[simp]
theorem snd_hnot [HNot α] [HNot β] (a : α × β) : (￢a).2 = ￢a.2 :=
  rfl

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