subset_lowerBounds_upperBounds — Mathlib

English

For any set s, s is contained in the set of lower bounds of the set of upper bounds of s.

Русский

Для любого множества s множество нижних границ множества верхних границ s содержит все элементы s.

LaTeX

$$s \subseteq \operatorname{lowerBounds}(\operatorname{upperBounds}(s))$$

Lean4

theorem subset_lowerBounds_upperBounds (s : Set α) : s ⊆ lowerBounds (upperBounds s) := fun _ hx _ hy => hy hx

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