mem_coprodᵢ_iff — Mathlib

English

A subset s of the product space belongs to the Coprodᵢ f iff for every i there is a t_i ∈ f i with eval i⁻¹(t_i) ⊆ s.

Русский

Множество s ⊆ ∏ α_i принадлежит Coprodᵢ f тогда и только тогда, когда для каждого i существует t_i ∈ f i с eval_i⁻¹(t_i) ⊆ s.

LaTeX

$$$\\forall s, s \\in Coprodᵢ f \\iff \\forall i, \\exists t_i \\in f i, \\; \\mathrm{eval}_i^{-1}(t_i) \\subseteq s$$$

Lean4

theorem mem_coprodᵢ_iff {s : Set (∀ i, α i)} : s ∈ Filter.coprodᵢ f ↔ ∀ i : ι, ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ s := by
  simp [Filter.coprodᵢ]

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