English
A bounded linear order becomes a bi-Heyting algebra by defining a→b and a\b piecewise, with complement given by aᶜ and top/bot as usual.
Русский
Замкнутый линейный порядок превращается в би-Хейтингову алгебру через покомпонентное определение a→b и a\b, комплементом служит aᶜ, ⊤ и ⊥ как обычно.
LaTeX
$$$\text{toBiheytingAlgebra}([ LinearOrder\ α ], [ BoundionedOrder\ α ]) : BiheytingAlgebra\ α$, где $a\to b = \text{условно } \top$ если $a\le b$, иначе $b$, и $a\setminus b = \bot$ если $a\le b$, иначе $a$; $\neg a = a^∗$ и т.д.$$
Lean4
/-- A bounded linear order is a bi-Heyting algebra by setting
* `a ⇨ b = ⊤` if `a ≤ b` and `a ⇨ b = b` otherwise.
* `a \ b = ⊥` if `a ≤ b` and `a \ b = a` otherwise. -/
abbrev toBiheytingAlgebra [LinearOrder α] [BoundedOrder α] : BiheytingAlgebra α :=
{ LinearOrder.toLattice, ‹BoundedOrder α› with himp := fun a b => if a ≤ b then ⊤ else b,
compl := fun a => if a = ⊥ then ⊤ else ⊥,
le_himp_iff := fun a b c => by
split_ifs with h
· exact iff_of_true le_top (inf_le_of_right_le h)
· rw [inf_le_iff, or_iff_left h],
himp_bot := fun _ => if_congr le_bot_iff rfl rfl, sdiff := fun a b => if a ≤ b then ⊥ else a,
hnot := fun a => if a = ⊤ then ⊥ else ⊤,
sdiff_le_iff := fun a b c => by
split_ifs with h
· exact iff_of_true bot_le (le_sup_of_le_left h)
· rw [le_sup_iff, or_iff_right h],
top_sdiff := fun _ => if_congr top_le_iff rfl rfl }
