partialSups_eq_biUnion_range — Mathlib

English

For s: Nat → Set α, n: Nat, partialSups s n equals the union over i in Finset.range(n+1) of s i.

Русский

Для s: Nat → Set α, n: Nat, partialSups s n равен объединению по i из Finset.range(n+1) множества s i.

LaTeX

$$$\partialSups s n = \bigcup_{i \in \operatorname{Finset.range}(n+1)} s i$$$

Lean4

theorem partialSups_eq_biUnion_range (s : ℕ → Set α) (n : ℕ) : partialSups s n = ⋃ i ∈ Finset.range (n + 1), s i := by
  simp [partialSups_eq_biSup, Nat.lt_succ]

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