of_subset_of_superset — Mathlib

English

If a is the least upper bound for s and for p, and s ⊆ t ⊆ p, then t has a as a least upper bound.

Русский

Если a — наименьшая верхняя граница для s и для p, и s ⊆ t ⊆ p, то t имеет a в качестве наименьшей верхней границы.

LaTeX

$${s t p : Set α} (hs : IsLUB s a) (hp : IsLUB p a) (hst : s ⊆ t) (htp : t ⊆ p) : IsLUB t a$$

Lean4

/-- If `a` is a least upper bound for sets `s` and `p`, then it is a least upper bound for any
set `t`, `s ⊆ t ⊆ p`. -/
theorem of_subset_of_superset {s t p : Set α} (hs : IsLUB s a) (hp : IsLUB p a) (hst : s ⊆ t) (htp : t ⊆ p) :
    IsLUB t a :=
  ⟨upperBounds_mono_set htp hp.1, lowerBounds_mono_set (upperBounds_mono_set hst) hs.2⟩

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