inf — Mathlib

English

If f is monotone on s, then f(x ∧ y) = f x ∧ f y for x,y ∈ s when appropriate.

Русский

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

LaTeX

$$$ [Preorder α] [SemilatticeInf β] {f : α → β} (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f(x ∧ y) = f(x) ∧ f(y)$$$

Lean4

/-- Pointwise infimum of two monotone functions is a monotone function. -/
protected theorem inf [Preorder α] [SemilatticeInf β] {f g : α → β} (hf : Antitone f) (hg : Antitone g) :
    Antitone (f ⊓ g) := fun _ _ h => inf_le_inf (hf h) (hg h)

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