Mathlib Map

Theorems · Definition · order theory

Sublattice.copy

{α : Type u_2} → [inst : Lattice α] → (L : Sublattice α) → (s : Set α) → s = ↑L → Sublattice α

Copy of a sublattice with a new carrier equal to the old one. Useful to fix definitional equalities.

Defined in
Mathlib.Order.Sublattice
Cited by
2 results in Mathlib
Foundations
Depth 11 from the axioms · uses no axioms
Assumes
Lattice
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BooleanSubalgebra.copy · cited by 2BooleanSubalgebra.copySublattice.LatticeHom.range · cited by 1LatticeHom.rangeSublattice.copy_eq · cited by 0Sublattice.copy_eqSublattice.coe_copy · cited by 0Sublattice.coe_copySet · cited by 53352SetSetLike.coe · cited by 8199SetLike.coeLattice · cited by 916LatticeSublattice · cited by 225SublatticeSublattice.copyCITED BYCITES

Cites4

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

  • Setstatement and proof · cited by 53,352
  • SetLike.coestatement and proof · cited by 8,199
  • Latticestatement and proof · cited by 916
  • Sublatticestatement and proof · cited by 225

Cited by4

Results whose statement or proof uses this declaration.