closure_iUnion₂_lt_nat — Mathlib

English

For a function f : ℕ → Set X, the closure distributes over finite initial unions: closure (⋃ m < n, f m) = ⋃ m < n, closure (f m).

Русский

Для функции f: ℕ → Set X замыкание распадается на конечные начальные объединения: closure (⋃ m < n, f m) = ⋃ m < n, closure (f m).

LaTeX

$$$\\\\overline{\\\\bigcup_{m < n} f(m)} = \\\\bigcup_{m < n} \\\\overline{f(m)}$$$

Lean4

@[simp]
theorem closure_iUnion₂_lt_nat {n : ℕ} (f : ℕ → Set X) : closure (⋃ m < n, f m) = ⋃ m < n, closure (f m) :=
  (finite_lt_nat n).closure_biUnion f

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