biInter_le_succ — Mathlib

English

For u: ℕ → Set α and n ∈ ℕ, the intersection over k ≤ n+1 equals the intersection over k ≤ n, intersected with u(n+1).

Русский

Пусть u: ℕ → Set α и n ∈ ℕ. Тогда ⋂_{k ≤ n+1} u_k = (⋂_{k ≤ n} u_k) ∩ u(n+1).

LaTeX

$$$\\displaystyle \\bigcap_{k \\le n+1} u(k) = \\bigcap_{k \\le n} u(k) \\cap u(n+1).$$$

Lean4

theorem biInter_le_succ (u : ℕ → Set α) (n : ℕ) : ⋂ k ≤ n + 1, u k = (⋂ k ≤ n, u k) ∩ u (n + 1) :=
  Nat.iInf_le_succ u n

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