of_map_sup — Mathlib

English

If a function f: α → β satisfies f(x ⊔ y) = f(x) ⊓ f(y) for all x,y ∈ s (under Sup/Inf duality), then f is antitone on s.

Русский

Если функция f: α → β удовлетворяет f(x ⊔ y) = f(x) ⊓ f(y) для всех x,y ∈ s (при двойственной связке Sup/Inf), то f антимонотонна на s.

LaTeX

$$[(∀ x ∈ s)(∀ y ∈ s) f(x ⊔ y) = f(x) ⊓ f(y)] ⇒ (∀ x ∈ s)(∀ y ∈ s) x ≤ y ⇒ f(x) ≥ f(y)$$

Lean4

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

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