subset_biUnion_of_mem

Mathlib.Data.Finset.Union

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

← MathLib Explorer

English

Let u: α → Finset β and x ∈ s. Then u(x) ⊆ s.biUnion u.

Русский

Пусть u: α → Finset β и x ∈ s. Тогда u(x) ⊆ s.biUnion u.

LaTeX

$$$\\forall {\\alpha\\,\\beta}, \\forall s : \\mathrm{Finset}(\\alpha), \\forall u : \\alpha \\to \\mathrm{Finset}(\\beta), \\forall x \\in s,\\; u(x) \\subseteq s.biUnion u$$$

Lean4

theorem subset_biUnion_of_mem (u : α → Finset β) {x : α} (xs : x ∈ s) : u x ⊆ s.biUnion u := by grind

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

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

Разделы

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

Аффилиация

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