iInter_eq_const

Mathlib.Data.Set.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

theorem iInter_eq_const (hf : ∀ i, f i = s) : ⋂ i, f i = s :=
  (iInter_congr hf).trans <| iInter_const _

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

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

Разделы

Аффилиация

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