iUnion_eq_const

Mathlib.Data.Set.Lattice

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

English

If ∀ i, f(i) = s, then ⋃_i f(i) = s.

Русский

Если для всех i выполняется f(i) = s, тогда ⋃_i f(i) = s.

LaTeX

$$$$ \\bigcup_{i} f(i) = s \\quad \\text{if } \\forall i,\\ f(i) = s $$$$

Lean4

theorem iUnion_eq_const (hf : ∀ i, f i = s) : ⋃ i, f i = s :=
  (iUnion_congr hf).trans <| iUnion_const _

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

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

Разделы

Аффилиация

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