Mathlib Map

Theorems · Definition · order theory

Equiv.supSet

{α : Type u_1} → {β : Type u_2} → α ≃ β → [SupSet β] → SupSet α

Transfer SupSet across an Equiv.

Defined in
Mathlib.Order.CompleteLattice.Defs
Cited by
1 results in Mathlib
Foundations
Depth 14 from the axioms · uses Quot.sound
Assumes
SupSet
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Equiv.completeLattice · cited by 0Equiv.completeLatticeEquiv.supSet_def · cited by 0Equiv.supSet_defDFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetEquiv · cited by 8337EquivEquiv.symm · cited by 3681Equiv.symmiSup · cited by 2415iSupSupSet · cited by 154SupSetEquiv.supSetCITED BYCITES

Cites6

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

  • DFunLike.coeproof · cited by 62,936
  • Setproof · cited by 53,352
  • Equivstatement and proof · cited by 8,337
  • Equiv.symmproof · cited by 3,681
  • iSupproof · cited by 2,415
  • SupSetstatement and proof · cited by 154

Cited by2

Results whose statement or proof uses this declaration.