eventually_subset_of_finite — Mathlib

English

If t is finite and for all a ∈ t we have a ∈ s i eventually as i varies in f, then eventually t ⊆ s i for all i with respect to f.

Русский

Если t конечно и для каждого a ∈ t выполняется, что a ∈ s i eventually по i, то в итоге выполняется t ⊆ s i для всех i по f.

LaTeX

$$$ ht : t.Finite \to ( \forall a \in t, \forall^{\!} i in f, a \in s i) \to \forall^{\!} i in f, t \subseteq s i $$$

Lean4

theorem eventually_subset_of_finite {ι : Type*} {f : Filter ι} {s : ι → Set α} {t : Set α} (ht : t.Finite)
    (hs : ∀ a ∈ t, ∀ᶠ i in f, a ∈ s i) : ∀ᶠ i in f, t ⊆ s i := by
  simpa [Set.subset_def, eventually_all_finite ht] using hs

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