union_lowerBounds_subset_lowerBounds_inter

English

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

Русский

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

LaTeX

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

Lean4

theorem union_lowerBounds_subset_lowerBounds_inter : lowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t) :=
  @union_upperBounds_subset_upperBounds_inter αᵒᵈ _ s t

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