partialSups_eq_sUnion_image — Mathlib

English

Under a decidable equality on sets, partialSups s n equals the union over the image of s restricted to range (n+1).

Русский

При наличии вычислимого равенства множеств, partialSups s n совпадает с объединением образа s на диапазоне (n+1).

LaTeX

$$$\partialSups s n = \bigcup_0 \uparrow\big( (\operatorname{Finset.range}(n+1)).\operatorname{image}s \big)$$$

Lean4

theorem partialSups_eq_sUnion_image [DecidableEq (Set α)] (s : ℕ → Set α) (n : ℕ) :
    partialSups s n = ⋃₀ ↑((Finset.range (n + 1)).image s) := by simp [partialSups_eq_biSup, Nat.lt_succ_iff]

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