mem_iUnion — Mathlib

English

An element x belongs to the union over i of s(i) iff there exists an index i with x ∈ s(i).

Русский

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

LaTeX

$$$(x \in \bigcup_{i} s(i)) \Leftrightarrow (\exists i, x \in s(i))$$$

Lean4

@[simp]
theorem mem_iUnion {x : α} {s : ι → Set α} : (x ∈ ⋃ i, s i) ↔ ∃ i, x ∈ s i :=
  ⟨fun ⟨_, ⟨⟨a, (t_eq : s a = _)⟩, (h : x ∈ _)⟩⟩ => ⟨a, t_eq.symm ▸ h⟩, fun ⟨a, h⟩ => ⟨s a, ⟨⟨a, rfl⟩, h⟩⟩⟩

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