mem_of_mem_toEnumFinset

Mathlib.Data.Multiset.Fintype

URI: https://scilib.ai/kg/mathlib#Multiset.mem_of_mem_toEnumFinset

← MathLib Explorer

English

If p belongs to m.toEnumFinset, then the first projection p.1 lies in m.

Русский

Если p ∈ m.toEnumFinset, то первая координата p.1 принадлежит m.

LaTeX

$$p ∈ m.toEnumFinset \Rightarrow p.1 ∈ m$$

Lean4

theorem mem_of_mem_toEnumFinset {p : α × ℕ} (h : p ∈ m.toEnumFinset) : p.1 ∈ m :=
  have := (m.mem_toEnumFinset p).mp h;
  Multiset.count_pos.mp (by cutsat)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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