iSup_partialSups_eq — Mathlib

English

In a complete lattice α, the iSup of partialSups f equals the iSup of f: ⨆ i, partialSups f i = ⨆ i, f i.

Русский

В полной решётке α верхнее объединение частичных верхушек совпадает с верхним объединением самих значений: ⨆ i, partialSups f i = ⨆ i, f i.

LaTeX

$$$\bigvee_i (\partialSups f i) = \bigvee_i f i$$$

Lean4

/-- Version of `ciSup_partialSups_eq` without boundedness assumptions, but requiring a
`CompleteLattice` rather than just a `ConditionallyCompleteLattice`. -/
theorem iSup_partialSups_eq (f : ι → α) : ⨆ i, partialSups f i = ⨆ i, f i :=
  ciSup_partialSups_eq <| OrderTop.bddAbove _

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