inter — Mathlib

English

If f and g are antitone on s, then the intersection 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) \cap g(x), s) $$$

Lean4

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

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