union_upperBounds_subset_upperBounds_inter

English

The union of upper bounds is contained in the upper bounds of the intersection: upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t).

Русский

Объединение верхних границ множества содержится в верхних границах их пересечения.

LaTeX

$$$\\mathrm{upperBounds}(s) \\cup \\mathrm{upperBounds}(t) \\subseteq \\mathrm{upperBounds}(s \\cap t)$$$

Lean4

theorem union_upperBounds_subset_upperBounds_inter : upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t) :=
  union_subset (upperBounds_mono_set inter_subset_left) (upperBounds_mono_set inter_subset_right)

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