iInter_mem' — Mathlib

English

Has the same form as biInter_mem' but with infinite index: (⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f under Subsingleton β.

Русский

Аналогично biInter_mem', но для iInter: (⋂ i, s i) ∈ f ⇔ ∀ i, s i ∈ f при Subsingleton β.

LaTeX

$$$(⋂ i, s i) \in f \iff \forall i, s i \in f$ (при Subsingleton β)$$

Lean4

/-- Weaker version of `Filter.iInter_mem` that assumes `Subsingleton β` rather than `Finite β`. -/
theorem iInter_mem' {β : Sort v} {s : β → Set α} [Subsingleton β] : (⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f := by
  rw [← sInter_range, sInter_eq_biInter, biInter_mem' (subsingleton_range s), forall_mem_range]

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