map_inf — Mathlib

English

A RelHom a preserves infimum: a(m ⊓ n) = a m ⊓ a n for all m,n in β, when a is a RelHom.

Русский

Гомоморфизм RelHom сохраняет наименьшее: a(m ∧ n) = a m ∧ a n для любых m,n.

LaTeX

$$$$ a(m \wedge n) = a m \wedge a n. $$$$

Lean4

theorem map_inf [SemilatticeInf α] [LinearOrder β] [FunLike F β α] [RelHomClass F (· < ·) (· < ·)] (a : F) (m n : β) :
    a (m ⊓ n) = a m ⊓ a n :=
  (StrictMono.monotone fun _ _ => map_rel a).map_inf m n

Похожие утверждения