le_map_sup — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem le_map_sup [SemilatticeSup α] [SemilatticeSup β] (f : α ↪o β) (x y : α) : f x ⊔ f y ≤ f (x ⊔ y) :=
  f.monotone.le_map_sup x y

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