height_top_eq_krullDim

fpvandoorn · Aug 2, 2024 · 19b26ca · 19b26ca
1 parent 37092da
commit 19b26ca
Showing 1 changed file with 9 additions and 4 deletions.
diff --git a/Carleson/ToMathlib/Height.lean b/Carleson/ToMathlib/Height.lean
@@ -522,10 +522,15 @@ lemma krullDim_eq_iSup_height : krullDim α = ⨆ (a : α), (height a : WithBot
     · rw [krullDim_eq_of_nonempty]
       simp only [WithBot.coe_le_coe, iSup_le_iff]
       intro x
-      apply height_le
-      intro p _
-      apply le_iSup_of_le p
-      simp only [le_refl]
+      exact height_le _ _ (fun p _ ↦ le_iSup_of_le p (le_refl _))
+
+@[simp]
+lemma height_top_eq_krullDim [OrderTop α] : height (⊤ : α) = krullDim α := by
+  rw [krullDim_eq_of_nonempty]
+  simp only [WithBot.coe_inj]
+  apply le_antisymm
+  · exact height_le _ _ (fun p _ ↦ le_iSup_of_le p (le_refl _))
+  · exact iSup_le (fun p => le_height_of_last_le ⊤ p le_top)
 
 
 /-! TODO: coheight -/