biInter_lt_succ — Mathlib

English

For a family of sets u: ℕ → Set α and n ∈ ℕ, the intersection over k < n+1 equals the intersection over k < n, together with u_n: ⋂ k < n+1, u_k = (⋂ k < n, u_k) ∩ u_n.

Русский

Для u: ℕ → Set α и n ∈ ℕ верно: ⋂_{k < n+1} u_k = (⋂_{k < n} u_k) ∩ u_n.

LaTeX

$$$\\displaystyle \\bigcap_{k < n+1} u_k = \\big(\\bigcap_{k < n} u_k\\big) \\cap u_n.$$$

Lean4

theorem biInter_lt_succ (u : ℕ → Set α) (n : ℕ) : ⋂ k < n + 1, u k = (⋂ k < n, u k) ∩ u n :=
  Nat.iInf_lt_succ u n

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