bddAbove_range_partialSups — Mathlib

English

The upper bounds of the range of partialSups f coincide with the upper bounds of the range of f.

Русский

Верхние границы множества значений partialSups f совпадают с верхними границами множества значений f.

LaTeX

$$$\\operatorname{upperBounds}(\\operatorname{Set.range}(\\mathrm{partialSups}\\, f)) = \\operatorname{upperBounds}(\\operatorname{Set.range} f)$$$

Lean4

@[simp]
theorem bddAbove_range_partialSups {f : ι → α} : BddAbove (Set.range (partialSups f)) ↔ BddAbove (Set.range f) :=
  .of_eq <| congr_arg Set.Nonempty <| upperBounds_range_partialSups f

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