iUnion_coe_set

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.iUnion_coe_set

English

Let s ⊆ α and f : s → Set β. Then ⋃ i f i equals ⋃ i ∈ s, f(⟨i, hi⟩).

Русский

Пусть s ⊆ α и f : s → Set β. Тогда ⋃ i f i равно ⋃ i ∈ s, f(⟨i, hi⟩).

LaTeX

$$$\\\\bigcup_{i} f(i) = \\\\bigcup_{i \\in s} f(\\\\langle i, \\\\iin s\\\\rangle)$$$

Lean4

@[simp]
theorem iUnion_coe_set {α β : Type*} (s : Set α) (f : s → Set β) : ⋃ i, f i = ⋃ i ∈ s, f ⟨i, ‹i ∈ s›⟩ :=
  iUnion_subtype _ _

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

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

Разделы

Аффилиация

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