upperBounds_mono — Mathlib

English

If s ⊆ t and a ≤ b, then a ∈ upperBounds t implies b ∈ upperBounds s.

Русский

Если s ⊆ t и a ≤ b, то если a является верхней границей t, то и b является верхней границей s.

LaTeX

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

Lean4

theorem upperBounds_mono ⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b⦄ (hab : a ≤ b) : a ∈ upperBounds t → b ∈ upperBounds s :=
  fun ha => upperBounds_mono_set hst <| upperBounds_mono_mem hab ha

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