iUnion_congr

Mathlib.Data.Set.Lattice

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

English

If s_i = t_i for every i, then the unions over i coincide: ⋃_i s_i = ⋃_i t_i.

Русский

Если для каждого i выполняется s_i = t_i, то ⋃_i s_i = ⋃_i t_i.

LaTeX

$$$$ \\left( \\forall i,\\ s_i = t_i \\right) \\Rightarrow \\bigcup_{i} s_i = \\bigcup_{i} t_i $$$$

Lean4

theorem iUnion_congr {s t : ι → Set α} (h : ∀ i, s i = t i) : ⋃ i, s i = ⋃ i, t i :=
  iSup_congr h

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

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

Разделы

Аффилиация

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