lowerBounds_mono_mem — Mathlib

English

If a ≤ b, then, for any s, if b ∈ lowerBounds s, then a ∈ lowerBounds s.

Русский

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

LaTeX

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

Lean4

theorem lowerBounds_mono_mem ⦃a b⦄ (hab : a ≤ b) : b ∈ lowerBounds s → a ∈ lowerBounds s := fun hb _ h =>
  le_trans hab (hb h)

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