Theorems · Inductive type · order theory

IsSublattice

{α : Type u_3} → [Lattice α] → Set α → Prop

A set s is a sublattice if a ⊔ b ∈ s and a ⊓ b ∈ s for all a ∈ s, b ∈ s. Note: This is not the preferred way to declare a sublattice. One should instead use Sublattice. TODO: Define Sublattice.

Defined in

Mathlib.Order.SupClosed

Cited by

28 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

Lattice