of_map_inf_le_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem of_map_inf_le_left [SemilatticeInf α] [Preorder β] {f : α → β} (h : ∀ x y, f (x ⊓ y) ≤ f x) : Monotone f :=
  by
  intro x y hxy
  rw [← inf_eq_right.2 hxy]
  apply h

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