Theorems · Theorem · order theory

RelHomClass.map_inf

∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : SemilatticeInf α] [inst_1 : LinearOrder β]
  [inst_2 : FunLike F β α] [RelHomClass F (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2] (a : F) (m n : β),
  a (min m n) = a m ⊓ a n

Defined in

Mathlib.Order.RelIso.Set

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemilatticeInfLinearOrderFunLikeRelHomClass