upperBounds_mono_set — Mathlib

English

Let α be a preorder. If s ⊆ t, then every upper bound of t is an upper bound of s.

Русский

Пусть α упорядочено по отношению предела. Если s ⊆ t, то любая верхняя граница t является верхней границей s.

LaTeX

$$$s \subseteq t \Rightarrow \operatorname{upperBounds}(t) \subseteq \operatorname{upperBounds}(s)$$$

Lean4

theorem upperBounds_mono_set ⦃s t : Set α⦄ (hst : s ⊆ t) : upperBounds t ⊆ upperBounds s := fun _ hb _ h => hb <| hst h

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