mem_inter

Mathlib.Data.Finset.Lattice.Basic

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

English

For any a, a ∈ s1 ∩ s2 if and only if a ∈ s1 and a ∈ s2.

Русский

Для любого элемента a верно: a ∈ s1 ∩ s2 тогда и только тогда, когда a ∈ s1 и a ∈ s2.

LaTeX

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

Lean4

@[simp, grind =]
theorem mem_inter {a : α} {s₁ s₂ : Finset α} : a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂ :=
  mem_ndinter

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

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

Разделы

Аффилиация

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