Theorems · Definition · order theory

Sublattice.prodEquiv

{α : Type u_2} →
  {β : Type u_3} →
    [inst : Lattice α] → [inst_1 : Lattice β] → (L : Sublattice α) → (M : Sublattice β) → ↥(L.prod M) ≃o ↥L × ↥M

The product of sublattices is isomorphic to their product as lattices.

Defined in

Mathlib.Order.Sublattice

Cited by

3 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

LatticeLattice