exists_finset_support

Mathlib.RingTheory.FreeCommRing

URI: https://scilib.ai/kg/mathlib#FreeCommRing.exists_finset_support

← MathLib Explorer

English

There exists a finite set s ⊆ α such that IsSupported(x, s).

Русский

Существует конечное множество s ⊆ α, такое что IsSupported(x, s).

LaTeX

$$$\\exists s : FiniteSet\\, \\alpha, \\mathrm{IsSupported}(x, s)$$$

Lean4

theorem exists_finset_support (x : FreeCommRing α) : ∃ s : Finset α, IsSupported x ↑s :=
  let ⟨s, hfs, hxs⟩ := exists_finite_support x
  ⟨hfs.toFinset, by rwa [Set.Finite.coe_toFinset]⟩

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

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

Разделы

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

Аффилиация

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