sSup_le_sSup_of_forall_exists_le — Mathlib

English

A deprecated alias states that if for every x in s there exists y in t with x ≤ y, then sSup(s) ≤ sSup(t).

Русский

Устаревшее утверждение: если для каждого x ∈ s существует y ∈ t с x ≤ y, то sSup(s) ≤ sSup(t).

LaTeX

$$$$ \\forall x \\in s, \\exists y \\in t, x \\le y \\; \\Rightarrow \\; \\operatorname{sSup}(s) \\le \\operatorname{sSup}(t) $$$$

Lean4

@[deprecated "use `sSup_le_sSup_of_isCofinalFor` instead" (since := "2025-07-14")]
theorem sSup_le_sSup_of_forall_exists_le (h : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) : sSup s ≤ sSup t :=
  sSup_le_sSup_of_isCofinalFor h

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