interior_iInter₂_le_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 \le n} f(m) \right) = \bigcap_{m \le n} interior (f(m))$$$

Lean4

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

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