lowerBounds_mono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lowerBounds_mono ⦃s t : Set α⦄ (hst : s ⊆ t) ⦃a b⦄ (hab : a ≤ b) : b ∈ lowerBounds t → a ∈ lowerBounds s :=
  fun hb => lowerBounds_mono_set hst <| lowerBounds_mono_mem hab hb

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