English
If α is a distributive lattice with bottom and sdiff is a difference operation satisfying sdiff(a,b) ≤ c ⇔ a ≤ b ⊔ c, then α becomes a Coheyting algebra with sdiff as given and hnot defined by hnot b = sdiff ⊤ b.
Русский
Если α — распределённая решетка с нижним элементом и операция разности sdiff удовлетворяет sdiff(a,b) ≤ c ⇔ a ≤ b ⊔ c, то α становится коейтинговой алгеброй, где sdiff задана, а hnot b = sdiff ⊤ b.
LaTeX
$$$ sdiff(a,b) \le c \iff a \le b \lor c $$$
Lean4
/-- Construct a co-Heyting algebra from the lattice structure and the difference alone. -/
abbrev ofSDiff [DistribLattice α] [BoundedOrder α] (sdiff : α → α → α)
(sdiff_le_iff : ∀ a b c, sdiff a b ≤ c ↔ a ≤ b ⊔ c) : CoheytingAlgebra α :=
{ ‹DistribLattice α›, ‹BoundedOrder α› with sdiff, hnot := fun a => sdiff ⊤ a, sdiff_le_iff,
top_sdiff := fun _ => rfl }
-- See note [reducible non-instances]
