of_map_sup — Mathlib

English

If f(x ⊔ y) = f(x) ⊔ f(y) for all x,y, then f is monotone.

Русский

Если f сохраняет верхнюю операцию: f(x ⊔ y) = f(x) ⊔ f(y), то f монотонна.

LaTeX

$$$ [SemilatticeSup \alpha] [SemilatticeSup \beta] \{f : \alpha \to \beta\} (h : \forall x y, f(x \lor y) = f(x) \lor f(y)) \Rightarrow Monotone f$$$

Lean4

theorem of_map_sup [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : ∀ x y, f (x ⊔ y) = f x ⊔ f y) : Monotone f :=
  (@of_map_inf (OrderDual α) (OrderDual β) _ _ _ h).dual

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