lint(various): nolint has_inhabited_instance for injective functions (#…

…4541)

`function.embedding`, `homeomorph`, `isometric` represent injective/bijective functions, so it's silly to expect them to be inhabited.

src/logic/embedding.lean

@@ -15,6 +15,7 @@ universes u v w x
 namespace function
 
 /-- `α ↪ β` is a bundled injective function. -/
+@[nolint has_inhabited_instance] -- depending on cardinalities, an injective function may not exist
 structure embedding (α : Sort*) (β : Sort*) :=
 (to_fun : α → β)
 (inj'   : injective to_fun)

src/topology/homeomorph.lean

@@ -10,6 +10,7 @@ open set
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 
 /-- α and β are homeomorph, also called topological isomoph -/
+@[nolint has_inhabited_instance] -- not all spaces are homeomorphic to each other
 structure homeomorph (α : Type*) (β : Type*) [topological_space α] [topological_space β]
   extends α ≃ β :=
 (continuous_to_fun  : continuous to_fun . tactic.interactive.continuity')

src/topology/metric_space/isometry.lean

@@ -111,6 +111,7 @@ lemma isometry.diam_range [metric_space α] [metric_space β] {f : α → β} (h
 by { rw ← image_univ, exact hf.diam_image univ }
 
 /-- `α` and `β` are isometric if there is an isometric bijection between them. -/
+@[nolint has_inhabited_instance] -- such a bijection need not exist
 structure isometric (α : Type*) (β : Type*) [emetric_space α] [emetric_space β]
   extends α ≃ β :=
 (isometry_to_fun  : isometry to_fun)