iSup_range

Mathlib.Order.CompleteLattice.Basic

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

English

Let g: β → α and f: ι → β. Then the supremum over b in range f of g(b) equals the supremum over i of g(f(i)).

Русский

Пусть g: β → α и f: ι → β. Тогда sup_{b ∈ range f} g(b) = sup_i g(f(i)).

LaTeX

$$$\\\\bigvee_{b \\in range f} g(b) = \\\\bigvee_i g(f(i))$$$

Lean4

theorem iSup_range {g : β → α} {f : ι → β} : ⨆ b ∈ range f, g b = ⨆ i, g (f i) := by rw [← iSup_subtype'', iSup_range']

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

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

Разделы

Аффилиация

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