isBounded_inter — Mathlib

English

If s is bounded below and t is bounded above, then s ∩ t is bounded.

Русский

Если s ограничено снизу, а t — сверху, то s ∩ t ограничено.

LaTeX

$$$\operatorname{BddBelow}(s) \rightarrow \operatorname{BddAbove}(t) \rightarrow \operatorname{IsBounded}(s \cap t)$$$

Lean4

theorem isBounded_inter (hs : BddBelow s) (ht : BddAbove t) : IsBounded (s ∩ t) :=
  (hs.mono inter_subset_left).isBounded <| ht.mono inter_subset_right

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