upperBounds_range_partialSups — Mathlib

English

partialSups is monotone in its argument: if f ≤ g, then partialSups f ≤ partialSups g.

Русский

partialSups монотонна по аргументу: если f ≤ g, то partialSups f ≤ partialSups g.

LaTeX

$$$\\text{Monotone}(f) \\Rightarrow \\text{Monotone}(\\mathrm{partialSups}\\, f)$$$

Lean4

@[simp]
theorem upperBounds_range_partialSups (f : ι → α) :
    upperBounds (Set.range (partialSups f)) = upperBounds (Set.range f) :=
  by
  ext a
  simp only [mem_upperBounds, Set.forall_mem_range, partialSups_le_iff]
  exact ⟨fun h _ ↦ h _ _ le_rfl, fun h _ _ _ ↦ h _⟩

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