Mathlib Map

Theorems · Theorem · logic and foundations

small_max

∀ (α : Type v), Small.{max w v, v} α

Due to https://github.com/leanprover/lean4/issues/2297, this is useless as an instance. See however Logic.UnivLE, whose API is able to indirectly provide this instance.

Defined in
Mathlib.Logic.Small.Defs
Cited by
3 results in Mathlib
Foundations
Depth 17 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.locallySmall_max · cited by 0CategoryTheory.locallySma…small_type · cited by 0small_typeunivLE_max · cited by 0univLE_maxSmall · cited by 369Smallsmall_lift · cited by 4small_liftsmall_maxCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by3

Results whose statement or proof uses this declaration.