Theorems · Definition · order theory

Sublattice.pi

{κ : Type u_5} →
  {π : κ → Type u_6} →
    [inst : (i : κ) → Lattice (π i)] → Set κ → ((i : κ) → Sublattice (π i)) → Sublattice ((i : κ) → π i)

Arbitrary product of sublattices. Given an index set s and a family of sublattices L : Π i, Sublattice (α i), pi s L is the sublattice of dependent functions f : Π i, α i such that f i belongs to L i whenever i ∈ s.

Defined in

Mathlib.Order.Sublattice

Cited by

9 results in Mathlib

Foundations

Depth 17 from the axioms · uses Quot.sound

Assumes

Lattice