of_map_inf — Mathlib

English

If a function f: α → β satisfies f(x ∧ y) = f(x) ∨ f(y) for all x,y ∈ s (in a semilattice-Inf/Inf setup), then f is antitone on s.

Русский

Если функция f: α → β удовлетворяет f(x ∧ y) = f(x) ∨ f(y) для всех x,y ∈ s (в условиях инф-суп), то 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_inf [SemilatticeInf α] [SemilatticeSup β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊔ f y) :
    AntitoneOn f s := fun x hx y hy hxy => sup_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]

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