mem_iInter — Mathlib

English

An element x belongs to the intersection over i of s(i) iff for every i, x ∈ s(i).

Русский

Элемент x принадлежит пересечению по i: x ∈ ⋂ i, s(i) тогда и только тогда, когда для каждого i верно x ∈ s(i).

LaTeX

$$$(x \in \bigcap_{i} s(i)) \Leftrightarrow (\forall i, x \in s(i))$$$

Lean4

@[simp]
theorem mem_iInter {x : α} {s : ι → Set α} : (x ∈ ⋂ i, s i) ↔ ∀ i, x ∈ s i :=
  ⟨fun (h : ∀ a ∈ {a : Set α | ∃ i, s i = a}, x ∈ a) a => h (s a) ⟨a, rfl⟩, fun h _ ⟨a, (eq : s a = _)⟩ => eq ▸ h a⟩

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