iInf_congr

Mathlib.Order.CompleteLattice.Basic

URI: https://scilib.ai/kg/mathlib#iInf_congr

English

If f i = g i for all i, then the infima are equal: ⨅ i f i = ⨅ i g i.

Русский

Если для всех i выполняется f(i) = g(i), то ⨅ i f(i) = ⨅ i g(i).

LaTeX

$$$$ (\forall i, f(i) = g(i)) \Rightarrow \bigwedge_i f(i) = \bigwedge_i g(i) $$$$

Lean4

theorem iInf_congr (h : ∀ i, f i = g i) : ⨅ i, f i = ⨅ i, g i :=
  congr_arg _ <| funext h

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

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

Разделы

Аффилиация

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