of_map_sup — Mathlib

English

If f preserves sup on all pairs from s, then f is monotone on s.

Русский

Если f сохраняет верхнюю операцию на всех парах из s, то она монотонна на s.

LaTeX

$$$ [SemilatticeSup \alpha] [SemilatticeSup \beta] (h : ∀ x ∈ s, ∀ y ∈ s, f(x ⊔ y) = f x ⊔ f y) : MonotoneOn f s$$$

Lean4

theorem of_map_sup [SemilatticeSup α] [SemilatticeSup β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊔ y) = f x ⊔ f y) :
    MonotoneOn f s :=
  (@of_map_inf αᵒᵈ βᵒᵈ _ _ _ _ h).dual

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