iSup_lt_eq_self — Mathlib

English

For any nonempty set s, a + ⨆ i∈s f_i = ⨆ i∈s (a + f_i).

Русский

Для любого непустого множества s: a + ⨆_{i∈s} f_i = ⨆_{i∈s} (a + f_i).

LaTeX

$$$a + \\sup_{i\\in s} f_i = \\sup_{i\\in s} (a + f_i)$$$

Lean4

@[simp]
theorem iSup_lt_eq_self (a : ℝ≥0∞) : ⨆ b, ⨆ _ : b < a, b = a :=
  by
  refine le_antisymm (iSup₂_le fun b hb ↦ hb.le) ?_
  refine le_of_forall_lt fun c hca ↦ ?_
  obtain ⟨d, hcd, hdb⟩ := exists_between hca
  exact hcd.trans_le <| le_iSup₂_of_le d hdb le_rfl

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