closure_iUnion₂_le_nat — Mathlib

English

For a function f : ℕ → Set X, the closure distributes over finite upper-bounded 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 \\le n} f(m)} = \\\\bigcup_{m \\le n} \\\\overline{f(m)}$$$

Lean4

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

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