map_sup — Mathlib

English

If f is an order-embedding that is an isomorphism between α and β, then f(x ∨ y) = f(x) ∨ f(y) for all x, y in α.

Русский

Если f — взаимно однозначное вложение порядка между α и β, то f(x ∨ y) = f(x) ∨ f(y) для любых x, y в α.

LaTeX

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

Lean4

theorem map_sup [SemilatticeSup α] [SemilatticeSup β] (f : α ≃o β) (x y : α) : f (x ⊔ y) = f x ⊔ f y :=
  f.dual.map_inf x y

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