chore(Topology): Inhabited -> Nonempty (#10647)

leanprover-community · Feb 17, 2024 · 996ae39 · 996ae39
1 parent 5a7ae92
commit 996ae39
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean b/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
@@ -222,8 +222,8 @@ private theorem dist_mem_candidates :
   exact ⟨fun x y => rfl, fun x y => rfl⟩
 
 /-- The distance on `X ⊕ Y` as a candidate -/
-def candidatesBDist (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Inhabited X]
-    [MetricSpace Y] [CompactSpace Y] [Inhabited Y] : Cb X Y :=
+def candidatesBDist (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X]
+    [MetricSpace Y] [CompactSpace Y] [Nonempty Y] : Cb X Y :=
   candidatesBOfCandidates _ dist_mem_candidates
 #align Gromov_Hausdorff.candidates_b_dist GromovHausdorff.candidatesBDist
 

diff --git a/Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean b/Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean
@@ -59,8 +59,8 @@ set_option linter.uppercaseLean3 false in
 -- Porting note : failed to derive `category`
 instance : Category (OpensLeCover U) := FullSubcategory.category _
 
-instance [Inhabited ι] : Inhabited (OpensLeCover U) :=
-  ⟨⟨⊥, default, bot_le⟩⟩
+instance [h : Nonempty ι] : Inhabited (OpensLeCover U) :=
+  ⟨⟨⊥, let ⟨i⟩ := h; ⟨i, bot_le⟩⟩⟩
 
 namespace OpensLeCover