Mathlib Map

Theorems · Definition · logic and foundations

Small.casesOn

{α : Type v} →
  {motive : Small.{w, v} α → Sort u} →
    (t : Small.{w, v} α) → ((equiv_small : ∃ S, Nonempty (α ≃ S)) → motive ⋯) → motive t
Defined in
Mathlib.Logic.Small.Defs
Cited by
4 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Cardinal.bddAbove_iff_small · cited by 3Cardinal.bddAbove_iff_sma…Cardinal.small_iff_lift_mk_lt_univ · cited by 1Cardinal.small_iff_lift_m…CategoryTheory.essentiallySmall_iff · cited by 1CategoryTheory.essentiall…small_iff · cited by 0small_iffEquiv · cited by 8337EquivSmall · cited by 369SmallSmall.casesOnCITED BYCITES

Cites2

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

  • Equivstatement and proof · cited by 8,337
  • Smallstatement and proof · cited by 369

Cited by4

Results whose statement or proof uses this declaration.