English
The interval type becomes a lattice whenever α is a lattice and a decidable order relation holds.
Русский
Тип интервалов образует решётку, если α — решётка и имеется разрешимое отношение порядка.
LaTeX
$$$$ \\text{Interval}(\\alpha) \\text{ is a lattice when } \\alpha \\text{ is a lattice and } \\text{DecidableLE}(\\alpha). $$$$
Lean4
instance lattice : Lattice (Interval α) :=
{
Interval.semilatticeSup with
inf := fun s t =>
match s, t with
| ⊥, _ => ⊥
| _, ⊥ => ⊥
| some s, some t =>
if h : s.fst ≤ t.snd ∧ t.fst ≤ s.snd then
WithBot.some ⟨⟨s.fst ⊔ t.fst, s.snd ⊓ t.snd⟩, sup_le (le_inf s.fst_le_snd h.1) <| le_inf h.2 t.fst_le_snd⟩
else ⊥
inf_le_left := fun s t =>
match s, t with
| ⊥, ⊥ => bot_le
| ⊥, some _ => bot_le
| some _, ⊥ => bot_le
| some s, some t => by
change dite _ _ _ ≤ _
split_ifs
· exact WithBot.coe_le_coe.2 ⟨le_sup_left, inf_le_left⟩
· exact bot_le
inf_le_right := fun s t =>
match s, t with
| ⊥, ⊥ => bot_le
| ⊥, some _ => bot_le
| some _, ⊥ => bot_le
| some s, some t => by
change dite _ _ _ ≤ _
split_ifs
· exact WithBot.coe_le_coe.2 ⟨le_sup_right, inf_le_right⟩
· exact bot_le
le_inf := fun s t c =>
match s, t, c with
| ⊥, _, _ => fun _ _ => bot_le
| (s : NonemptyInterval α), t, c => fun hb hc =>
by
lift t to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hb
lift c to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hc
change _ ≤ dite _ _ _
simp only [WithBot.coe_le_coe] at hb hc ⊢
rw [dif_pos, WithBot.coe_le_coe]
·
exact
⟨sup_le hb.1 hc.1, le_inf hb.2 hc.2⟩
-- Porting note: had to add the next 6 lines including the changes because
-- it seems that lean cannot automatically turn `NonemptyInterval.toDualProd s`
-- into `s.toProd` anymore.
rcases hb with ⟨hb₁, hb₂⟩
rcases hc with ⟨hc₁, hc₂⟩
change t.toProd.fst ≤ s.toProd.fst at hb₁
change s.toProd.snd ≤ t.toProd.snd at hb₂
change c.toProd.fst ≤ s.toProd.fst at hc₁
change s.toProd.snd ≤ c.toProd.snd at hc₂
exact ⟨hb₁.trans <| s.fst_le_snd.trans hc₂, hc₁.trans <| s.fst_le_snd.trans hb₂⟩ }
