map_ciSup' — Mathlib

English

An alternative form of CiSup for sets: the image of the supremum over a set equals the supremum of the images, under conditions of boundedness.

Русский

Альтернативная форма сохранения ciSup для множества: образ суммы верхних границ равен сумме верхних границ образов.

LaTeX

$$$e\\left( iSup\\{ f(i) : i\\in s\\} \\right) = iSup\\{ e(f(i)) : i\\in s\\}$$$

Lean4

@[simp]
theorem map_ciSup' (e : α ≃o β) (f : ι → α) : e (⨆ i, f i) = ⨆ i, e (f i) :=
  by
  cases isEmpty_or_nonempty ι
  · simp [map_bot]
  by_cases hf : BddAbove (range f)
  · exact e.map_ciSup hf
  · have hfe : ¬BddAbove (range fun i ↦ e (f i)) := by
      simpa [Set.Nonempty, BddAbove, upperBounds, e.surjective.forall] using hf
    simp [map_bot, hf, hfe]

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