biInter_mem' — Mathlib

English

Weaker version: if is is Subsingleton, then (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f.

Русский

Слабая версия: если is — подмножество-одиночное, то (⋂ i ∈ is, s i) ∈ f ⇔ ∀ i ∈ is, s i ∈ f.

LaTeX

$$$\text{If } is.\text{Subs singleton},\ (⋂ i \in is, s i) \in f \iff \forall i \in is, s i \in f$$$

Lean4

/-- Weaker version of `Filter.biInter_mem` that assumes `Subsingleton β` rather than `Finite β`. -/
theorem biInter_mem' {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Subsingleton) :
    (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f := by apply Subsingleton.induction_on hf <;> simp

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