map_inf_le — Mathlib

English

Let α and β be inf-semilattices and f: α → β be monotone. Then for all x, y ∈ α, f(x ∧ y) ≤ f(x) ∧ f(y).

Русский

Пусть α и β — полусуп-решётки по инф-операции, f: α → β монотонна. Тогда для любых x, y ∈ α выполняется f(x ∧ y) ≤ f(x) ∧ f(y).

LaTeX

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

Lean4

theorem map_inf_le [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : Monotone f) (x y : α) :
    f (x ⊓ y) ≤ f x ⊓ f y :=
  le_inf (h inf_le_left) (h inf_le_right)

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