feat: ¬ UnivLE.{u+1, u} (#5739)

Thanks to @kmill on [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Universe.20inequalities/near/372570044). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jul 6, 2023 · e28ad88 · e28ad88
1 parent 93bf611
commit e28ad88
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/Mathlib/Logic/Small/Basic.lean b/Mathlib/Logic/Small/Basic.lean
@@ -28,7 +28,7 @@ universe u w v
 
 /-- A type is `Small.{w}` if there exists an equivalence to some `S : Type w`.
 -/
-class Small (α : Type v) : Prop where
+@[mk_iff] class Small (α : Type v) : Prop where
   /-- If a type is `Small.{w}`, then there exists an equivalence with some `S : Type w` -/
   equiv_small : ∃ S : Type w, Nonempty (α ≃ S)
 #align small Small

diff --git a/Mathlib/Logic/UnivLE.lean b/Mathlib/Logic/UnivLE.lean
@@ -47,3 +47,7 @@ example : UnivLE.{u, max u v} := inferInstance
 instance [UnivLE.{u, v}] (α : Type u) : Small.{v} α :=
   ⟨Shrink.{v, max u v} (ULift.{v} α),
     ⟨Equiv.ulift.symm.trans (equivShrink (ULift α))⟩⟩
+
+example : ¬ UnivLE.{u+1, u} := by
+  simp only [Small_iff, not_forall, not_exists, not_nonempty_iff]
+  exact ⟨Type u, fun α => ⟨fun f => Function.not_surjective_Type.{u, u} f.symm f.symm.surjective⟩⟩