upperBounds_mono_of_isCofinalFor — Mathlib

English

If s ⊆ t and IsCofinalFor s t, then every upper bound of t is an upper bound of s.

Русский

Пусть s ⊆ t и IsCofinalFor s t. Тогда каждая верхняя граница t является верхней границей s.

LaTeX

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

Lean4

@[gcongr]
theorem upperBounds_mono_of_isCofinalFor (hst : IsCofinalFor s t) : upperBounds t ⊆ upperBounds s := fun _a ha _b hb ↦
  let ⟨_c, hc, hbc⟩ := hst hb;
  hbc.trans (ha hc)

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