iSup_congr

Mathlib.Order.CompleteLattice.Basic

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

English

If f and g are pointwise equal, then their supremums are equal: ⨆ i, f i = ⨆ i, g i.

Русский

Если f(i) = g(i) для каждого i, то ⨆ i f(i) = ⨆ i g(i).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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