Mathlib Map

Theorems · Definition · order theory

Equiv.infSet

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

Transfer InfSet 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
InfSet
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Equiv.infSet_def · cited by 0Equiv.infSet_defEquiv.completeLattice · cited by 0Equiv.completeLatticeDFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetEquiv · cited by 8337EquivEquiv.symm · cited by 3681Equiv.symmiInf · cited by 1690iInfInfSet · cited by 145InfSetEquiv.infSetCITED 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
  • iInfproof · cited by 1,690
  • InfSetstatement and proof · cited by 145

Cited by2

Results whose statement or proof uses this declaration.