From 7fb9d9aa19e1d275e6d008be0571125453af45d7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 24 Jun 2026 13:30:27 -0500 Subject: [PATCH] Clean up Lattice.lean's namespaces Signed-off-by: Danila Fedorin --- lean/Spa/Lattice.lean | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/lean/Spa/Lattice.lean b/lean/Spa/Lattice.lean index 1ed2cdf..d50c8fa 100644 --- a/lean/Spa/Lattice.lean +++ b/lean/Spa/Lattice.lean @@ -61,12 +61,11 @@ class FiniteHeightLattice (α : Type*) [Lattice α] extends Bot α, Top α where longestChain : PointedLTSeries α ⊥ ⊤ height chains_bounded : BoundedChains α height -namespace FixedHeight +namespace FiniteHeightLattice -variable {α : Type*} [Lattice α] {h : ℕ} +variable (α : Type*) [Lattice α] [FiniteHeightLattice α] -theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by - intro a +theorem bot_le (a : α) : (⊥ : α) ≤ a := by by_cases heq : ⊥ ⊓ a = ⊥ · exact inf_eq_left.mp heq · exfalso @@ -78,14 +77,6 @@ theorem bot_le [FiniteHeightLattice α] : ∀ (a : α), ⊥ ≤ a := by rw [RelSeries.cons_length, lc.length_series] at hbound omega -end FixedHeight - -namespace FiniteHeightLattice - -variable (α : Type*) [Lattice α] [FiniteHeightLattice α] - -theorem bot_le (a : α) : (⊥ : α) ≤ a := FixedHeight.bot_le a - end FiniteHeightLattice end Spa