iInter_congr

Mathlib.Data.Set.Lattice

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

English

If s_i = t_i for every i, then the intersections 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 \\bigcap_{i} s_i = \\bigcap_{i} t_i $$$$

Lean4

theorem iInter_congr {s t : ι → Set α} (h : ∀ i, s i = t i) : ⋂ i, s i = ⋂ i, t i :=
  iInf_congr h

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

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

Разделы

Аффилиация

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