mem_inter_of_mem

Mathlib.Data.Finset.Lattice.Basic

URI: https://scilib.ai/kg/mathlib#Finset.mem_inter_of_mem

English

If a ∈ s1 and a ∈ s2 then a ∈ s1 ∩ s2.

Русский

Если a принадлежит S1 и a принадлежит S2, то a принадлежит S1 ∩ S2.

LaTeX

$$$a \\in s_{1} \\land a \\in s_{2} \\Rightarrow a \\in s_{1} \\cap s_{2}$$$

Lean4

theorem mem_inter_of_mem {a : α} {s₁ s₂ : Finset α} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂ :=
  and_imp.1 mem_inter.2

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

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

Разделы

Аффилиация

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