map_inf_le — Mathlib

English

Let f be an order-embedding between semilattices with inf. Then for all x, y in the domain, f(x ∧ y) ≤ f(x) ∧ f(y).

Русский

Пусть f является вложением порядка между полулежаниями с операцией meet. Тогда для любых x, y верно: f(x ∧ y) ≤ f(x) ∧ f(y).

LaTeX

$$$ f(x \wedge y) \le f(x) \wedge f(y) $$$

Lean4

theorem map_inf_le [SemilatticeInf α] [SemilatticeInf β] (f : α ↪o β) (x y : α) : f (x ⊓ y) ≤ f x ⊓ f y :=
  f.monotone.map_inf_le x y

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