Theorems · Definition · order theory

Sublattice.carrier

{α : Type u_2} → [inst : Lattice α] → Sublattice α → Set α

The underlying set of a sublattice. Do not use directly. Instead, use the coercion Sublattice α → Set α, which Lean should automatically insert for you in most cases.

Defined in

Mathlib.Order.Sublattice

Cited by

23 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

Lattice