union — Mathlib

English

If f and g are monotone on s, then 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) \cup g(x), s) $$$

Lean4

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

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