compl_mem_coprodᵢ — Mathlib

English

Complement membership in Coprodᵢ f is characterized by the complements of images under evaluation maps.

Русский

Членство дополнения в Coprodᵢ f описывается через дополнения образов под отображениями оценки.

LaTeX

$$$s^{\\complement} \\in Coprodᵢ f \\iff \\forall i, (eval_i' s)^{\\complement} \\in f i$$$

Lean4

theorem compl_mem_coprodᵢ {s : Set (∀ i, α i)} : sᶜ ∈ Filter.coprodᵢ f ↔ ∀ i, (eval i '' s)ᶜ ∈ f i := by
  simp only [Filter.coprodᵢ, mem_iSup, compl_mem_comap]

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