coe_sSup' — Mathlib

English

For SupSet α, if s is bounded above, the embedding of sSup s equals the supremum in WithTop of the image of s under the embedding.

Русский

Для SupSet α, если s ограничено сверху, вложение sSup s равно верхней грани в WithTop от образа s через вложение.

LaTeX

$$$$ \uparrow\bigl( \operatorname{sSup} s \bigr) = \operatorname{sSup}\bigl( \{ \uparrow a \mid a \in s \} \bigr). $$$$

Lean4

theorem coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) : ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α) :=
  by
  classical
  change _ = ite _ _ _
  rw [if_neg, preimage_image_eq, if_pos hs]
  · exact Option.some_injective _
  · rintro ⟨x, _, ⟨⟩⟩

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