iSup_eq_iSup_of_partialSups_eq_partialSups

Mathlib.Order.PartialSups

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

← MathLib Explorer

English

If partialSups f = partialSups g, then iSup f = iSup g.

Русский

Если partialSups f = partialSups g, то ∎suprema f = suprema g.

LaTeX

$$$\text{partialSups } f = \text{partialSups } g \Rightarrow \bigvee_i f(i) = \bigvee_i g(i)$$$

Lean4

theorem iSup_eq_iSup_of_partialSups_eq_partialSups {f g : ι → α} (h : partialSups f = partialSups g) :
    ⨆ i, f i = ⨆ i, g i := by simp_rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g, h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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