eventually — Mathlib

English

For any restricted product, almost every coordinate lies in the corresponding set A_i.

Русский

Для любого ограниченного произведения почти на всех координатах выполняется x_i ∈ A_i.

LaTeX

$$$\\forall x \\in \\mathrm{RestrictedProduct}(R_i, A_i, 𝓕),\\; \\forall^\\infty i \\in 𝓕,\\; x_i \\in A_i.$$$

Lean4

@[simp]
theorem eventually (x : Πʳ i, [R i, A i]_[𝓕]) : ∀ᶠ i in 𝓕, x i ∈ A i :=
  x.2

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