of_map_inf_le — Mathlib

English

If for all x, y we have f(x ∧ y) ≤ f(x) ∧ f(y), then f is monotone.

Русский

Если для всех x, y выполняется f(x ∧ y) ≤ f(x) ∧ f(y), то функция монотонна.

LaTeX

$$$ [SemilatticeInf \alpha] [SemilatticeInf \beta] \{f : \alpha \to \beta\} (h : \forall x y, f(x \wedge y) \le f(x) \wedge f(y)) \Rightarrow Monotone f$$$

Lean4

theorem of_map_inf_le [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : ∀ x y, f (x ⊓ y) ≤ f x ⊓ f y) :
    Monotone f :=
  of_map_inf_le_left fun x y ↦ (h x y).trans inf_le_left

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