English
The class LocallyFiniteOrderBot α is a Subsingleton; any two such bottom-structured orders coincide.
Русский
Класс LocallyFiniteOrderBot α является Subsingleton; любые две такие структуры совпадают.
LaTeX
$$$\operatorname{Subsingleton}(\mathrm{LocallyFiniteOrderBot}(\alpha))$$$
Lean4
instance : Subsingleton (LocallyFiniteOrderBot α) :=
Subsingleton.intro fun h₀ h₁ =>
by
obtain ⟨h₀_finset_Iio, h₀_finset_Iic, h₀_finset_mem_Iic, h₀_finset_mem_Iio⟩ := h₀
obtain ⟨h₁_finset_Iio, h₁_finset_Iic, h₁_finset_mem_Iic, h₁_finset_mem_Iio⟩ := h₁
have hIic : h₀_finset_Iic = h₁_finset_Iic := by
ext a b
rw [h₀_finset_mem_Iic, h₁_finset_mem_Iic]
have hIio : h₀_finset_Iio = h₁_finset_Iio := by
ext a b
rw [h₀_finset_mem_Iio, h₁_finset_mem_Iio]
simp_rw [hIic, hIio]
-- Should this be called `LocallyFiniteOrder.lift`?
