inter — Mathlib

English

If f and g are antitone on s, then the union map 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 inter [Preorder β] {f g : β → Set α} {s : Set β} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
    AntitoneOn (fun x => f x ∩ g x) s :=
  hf.inf hg

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