Theorems · Theorem · order theory

InfHomClass.map_inf

∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Min α} {inst_1 : Min β} {inst_2 : FunLike F α β}
  [self : InfHomClass F α β] (f : F) (a b : α), f (a ⊓ b) = f a ⊓ f b

An InfHomClass morphism preserves infima.

Defined in

Mathlib.Order.Hom.Lattice

Cited by

20 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

InfHomClass