Theorems · Theorem · order theory

Sublattice.map_inf

∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L M : Sublattice α) (f : LatticeHom α β),
  Function.Injective ⇑f → Sublattice.map f (L ⊓ M) = Sublattice.map f L ⊓ Sublattice.map f M

Defined in

Mathlib.Order.Sublattice

Cited by

0 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LatticeLattice