map_inf — Mathlib

English

If for all x ∈ s, y ∈ s we have f(x ⊔ y) = f x ⊔ f y, then f is monotone on s.

Русский

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

LaTeX

$$$ [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : ∀ x ∈ s, ∀ y ∈ s, f(x ⊔ y) = f x ⊔ f y) : MonotoneOn f s$$$

Lean4

theorem map_inf [SemilatticeInf β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (x ⊓ y) = f x ⊓ f y :=
  hf.dual.map_sup hx hy

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