mem_iInter₂_of_mem

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.mem_iInter₂_of_mem

English

If a ∈ s(i, j) for all i and j, then a ∈ ⋂ (i) (j), s i j.

Русский

Если для всех i и j выполняется a ∈ s(i, j), то a ∈ ⋂ (i) (j), s i j.

LaTeX

$$$(\\\\forall i \\\\forall j, a \\\\in s(i,j)) \\\\Rightarrow a \\\\in \\\\bigcap_{i}\\bigcap_{j} s(i,j)$$$

Lean4

theorem mem_iInter₂_of_mem {s : ∀ i, κ i → Set α} {a : α} (h : ∀ i j, a ∈ s i j) : a ∈ ⋂ (i) (j), s i j :=
  mem_iInter₂.2 h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru