inter — Mathlib

English

If f and g are monotone on s, then the intersection map x ↦ f(x) ∩ g(x) is monotone on s.

Русский

Если f и g монотонны на s, то x ↦ f(x) ∩ g(x) монотонна на s.

LaTeX

$$$ \operatorname{MonotoneOn}(f,s) \land \operatorname{MonotoneOn}(g,s) \Rightarrow \operatorname{MonotoneOn}(x \mapsto f(x) \cap g(x), s) $$$

Lean4

theorem inter [Preorder β] {f g : β → Set α} {s : Set β} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
    MonotoneOn (fun x => f x ∩ g x) s :=
  hf.inf hg

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