interior_iInter₂_lt_nat — Mathlib

English

For a natural n, interior of the intersection over m < n equals the intersection of interiors over m < n.

Русский

Для натурального n: interior(⋂ m < n, f(m)) = ⋂ m < n, interior(f(m)).

LaTeX

$$$ \forall n \in \mathbb{N},\ (f: \mathbb{N} \to Set X) :\ interior \left( \bigcap_{m < n} f(m) \right) = \bigcap_{m < n} interior (f(m))$$$

Lean4

@[simp]
theorem interior_iInter₂_lt_nat {n : ℕ} (f : ℕ → Set X) : interior (⋂ m < n, f m) = ⋂ m < n, interior (f m) :=
  (finite_lt_nat n).interior_biInter f

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