union — Mathlib

English

If f and g are antitone on s, then x ↦ f(x) ∪ g(x) is antitone on s.

Русский

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

LaTeX

$$$ \operatorname{AntitoneOn}(f,s) \land \operatorname{AntitoneOn}(g,s) \Rightarrow \operatorname{AntitoneOn}(x \mapsto f(x) \cup g(x), s) $$$

Lean4

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

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