isLeast_hnot — Mathlib

English

In a co-Heyting algebra, the negation ¬a is the least element w such that Codisjoint a w.

Русский

В коейтейтинговой алгебре отрицание ¬a есть наименьшее w такое, что Codisjoint a w.

LaTeX

$$IsLeast {w | Codisjoint a w} (¬a)$$

Lean4

theorem isLeast_hnot [CoheytingAlgebra α] (a : α) : IsLeast {w | Codisjoint a w} (￢a) := by
  simpa only [CoheytingAlgebra.top_sdiff, codisjoint_iff_le_sup] using isLeast_sdiff ⊤ a

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