mem_iInter₂ — Mathlib

English

Let x belong to the intersection over i and j of s(i, j). Then for every i and j, x ∈ s(i, j); conversely, if x ∈ s(i, j) for all i and j, then x lies in the intersection.

Русский

Пусть x принадлежит пересечению по всем i и j множеств s(i, j); тогда для всех i, j выполняется x ∈ s(i, j); и наоборот, если для всех i, j x ∈ s(i, j), то x принадлежит пересечению.

LaTeX

$$$x \\in \\bigcap_i \\bigcap_j s(i,j) \\iff \\forall i \\forall j, x \\in s(i,j)$$$

Lean4

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

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