mem_iUnion₂ — Mathlib

English

Let x be an element of the union over i of the unions over j of s(i, j). Then there exist indices i and j with x ∈ s(i, j).

Русский

Пусть x принадлежит объединению по i затем по j множеств s(i, j). Тогда существуют индексы i и j такие, что x ∈ s(i, j).

LaTeX

$$$x \\\\in \\\\bigcup_i \\\\bigcup_j s(i,j) \iff \\\\exists i \\\\exists j, x \\\\in s(i,j)$$$

Lean4

theorem mem_iUnion₂ {x : γ} {s : ∀ i, κ i → Set γ} : (x ∈ ⋃ (i) (j), s i j) ↔ ∃ i j, x ∈ s i j := by
  simp_rw [mem_iUnion]

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