of_map_inf — Mathlib

English

If f satisfies f(x ∧ y) = f x ∧ f y for all x,y in s, then f is monotone on s.

Русский

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

LaTeX

$$$ [SemilatticeInf \alpha] [SemilatticeInf \beta] {f : \alpha → \beta} (h : ∀ x ∈ s, ∀ y ∈ s, f(x ∧ y) = f x ∧ f y) : MonotoneOn f s$$$

Lean4

theorem of_map_inf [SemilatticeInf α] [SemilatticeInf β] (h : ∀ x ∈ s, ∀ y ∈ s, f (x ⊓ y) = f x ⊓ f y) :
    MonotoneOn f s := fun x hx y hy hxy => inf_eq_left.1 <| by rw [← h _ hx _ hy, inf_eq_left.2 hxy]

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