English
If α is a distributive lattice with bottom and there is a function hnot such that a ∧ hnot b ≤ c ⇔ a ≤ b ⊔ c, then α forms a Coheyting algebra with sdiff(a,b) := a ∧ hnot b.
Русский
Если α — распределённая решетка с нулём и существует функция hnot такая, что a ∧ hnot b ≤ c ⇔ a ≤ b ⊔ c, то α образует коейтинговую алгебру; sdiff(a,b) = a ∧ hnot b.
LaTeX
$$$ a \land \mathrm{hnot}(b) \le c \iff a \le b \lor c $$$
Lean4
/-- Construct a co-Heyting algebra from the difference and Heyting negation alone. -/
abbrev ofHNot [DistribLattice α] [BoundedOrder α] (hnot : α → α) (sdiff_le_iff : ∀ a b c, a ⊓ hnot b ≤ c ↔ a ≤ b ⊔ c) :
CoheytingAlgebra α where
sdiff a b := a ⊓ hnot b
hnot := hnot
sdiff_le_iff := sdiff_le_iff
top_sdiff _ := top_inf_eq _
