of_map_inf — Mathlib

English

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

Русский

Если для всех x, y выполняется f(x ∧ y) = f(x) ∧ f(y), то f — монотонна.

LaTeX

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

Lean4

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

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