upperBounds_mono_mem — Mathlib

English

If a ≤ b, then, for any s, if a is an upper bound of s, then b is an upper bound of s.

Русский

Если a ≤ b, то для любого множества s, если a является верхней границей s, то и b является верхней границей s.

LaTeX

$$a \le b \Rightarrow (a \in \operatorname{upperBounds}(s) \Rightarrow b \in \operatorname{upperBounds}(s))$$

Lean4

theorem upperBounds_mono_mem ⦃a b⦄ (hab : a ≤ b) : a ∈ upperBounds s → b ∈ upperBounds s := fun ha _ h =>
  le_trans (ha h) hab

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