partialSups_eq_biSup — Mathlib

English

For complete lattice α, f: ι → α, iSup of partialSups f i equals iSup of f i, i.e., partialSups f i = ⨆ j ≤ i, f j.

Русский

Для полной решётки α, ⨆ i (partialSups f i) = ⨆ i f i – эквивалентно: partialSups f i = ⨆ { j ≤ i } f j.

LaTeX

$$$\operatorname{partialSups} f\, i = \bigvee_{j \le i} f(j)$$$

Lean4

theorem partialSups_eq_biSup (f : ι → α) (i : ι) : partialSups f i = ⨆ j ≤ i, f j := by
  simpa only [iSup_subtype] using partialSups_eq_ciSup_Iic f i

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