inter — Mathlib

English

If f and g are monotone as maps to sets, then the pointwise intersection x ↦ f(x) ∩ g(x) is monotone.

Русский

Если f и g являются монотонными отображениями в множества, то функция x ↦ f(x) ∩ g(x) монотонна по x.

LaTeX

$$$ \operatorname{Monotone}(f) \land \operatorname{Monotone}(g) \Rightarrow \operatorname{Monotone}(x \mapsto f(x) \cap g(x)) $$$

Lean4

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

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