iSup_split_single — Mathlib

English

If s ⊆ t, then the supremum over s is less than or equal to the supremum over t: ⨆ x ∈ s, f x ≤ ⨆ x ∈ t, f x.

Русский

Если s ⊆ t, тогда супремум по s не превышает супремум по t: ⨆ x ∈ s f x ≤ ⨆ x ∈ t f x.

LaTeX

$$$$ \\sup_{x \\in s} f(x) \\leq \\sup_{x \\in t} f(x) \\quad \\text{if } s \\subseteq t $$$$

Lean4

theorem iSup_split_single (f : β → α) (i₀ : β) : ⨆ i, f i = f i₀ ⊔ ⨆ (i) (_ : i ≠ i₀), f i :=
  by
  convert iSup_split f (fun i => i = i₀)
  simp

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