subset_set_biUnion_of_mem

Mathlib.Order.CompleteLattice.Finset

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

← MathLib Explorer

English

If x is in s and f(x) is a set, then f(x) is contained in the union over all y in s of f(y).

Русский

Если x ∈ s и f(x) — множество, то f(x) ⊆ ⋃_{y∈s} f(y).

LaTeX

$$$$ f(x) \\subseteq \\bigcup_{y \\in s} f(y) $$$$

Lean4

theorem subset_set_biUnion_of_mem {s : Finset α} {f : α → Set β} {x : α} (h : x ∈ s) : f x ⊆ ⋃ y ∈ s, f y :=
  show f x ≤ ⨆ y ∈ s, f y from le_iSup_of_le x <| by simp only [h, iSup_pos, le_refl]

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

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

Разделы

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

Аффилиация

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