English
If α is a distributive lattice with bottom and a binary operation himp satisfies the adjunction a ≤ himp b c ⇔ a ∧ b ≤ c, then α can be endowed with a Heyting algebra structure with himp as given and compl defined by compl(a) = himp(a, ⊥).
Русский
Если α — распределённая решетка с нулём и имеется бинарная операция himp, удовлетворяющая сопряжённости a ≤ himp b c ⇔ a ∧ b ≤ c, то α можно наделить структурой HeytingAlgebra с данным himp и определением compl(a) = himp(a, ⊥).
LaTeX
$$$ \exists himp:\alpha\to\alpha\to\alpha\,\bigl(\forall a,b,c\in\alpha,\n a\le himp(b,c) \iff a\wedge b \le c\bigr) \Rightarrow \text{HeytingAlgebra } \alpha $$$
Lean4
/-- Construct a Heyting algebra from the lattice structure and complement operator alone. -/
abbrev ofCompl [DistribLattice α] [BoundedOrder α] (compl : α → α)
(le_himp_iff : ∀ a b c, a ≤ compl b ⊔ c ↔ a ⊓ b ≤ c) : HeytingAlgebra α
where
himp := (compl · ⊔ ·)
compl := compl
le_himp_iff := le_himp_iff
himp_bot
_ :=
sup_bot_eq
_
-- See note [reducible non-instances]
