biInter_lt_succ'

Mathlib.Data.Nat.Lattice

URI: https://scilib.ai/kg/mathlib#Set.biInter_lt_succ'

English

For u: ℕ → Set α and n ∈ ℕ, the intersection over k < n+1 equals u0 intersect the intersection over k < n of u(k+1).

Русский

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

LaTeX

$$$\\displaystyle \\bigcap_{k < n+1} u_k = u_0 \\cap \\bigcap_{k < n} u_{k+1}.$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru