map_csSup' — Mathlib

English

Let e be an order isomorphism α ≃o β. For any nonempty s ⊆ α that is bounded above, e(sSup s) = ⨆ x ∈ s, e x.

Русский

Пусть e — биекция порядка α ≃o β. Для непустого ограниченного сверху множества s ⊆ α выполняется e( Sup s ) = Sup { e(x) : x ∈ s }.

LaTeX

$$$ e(\mathrm{sSup} s) = \big( \vee_{x \in s} e(x) \big) $$$

Lean4

theorem map_csSup' (e : α ≃o β) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : e (sSup s) = sSup (e '' s) :=
  e.to_galoisConnection.l_csSup' hne hbdd

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